Functional Programming and Type Theory | ChungAng University, Fall 2003 |

Homework in Lambda Calculus | |

- Evaluate the following lambda calculus expressions to normal
form. If no normal form exists, explain why.
- (\x. \y. x x y) (\x. x x)
- (\x. \y. x (x y)) (\x. x x)
- (\x. (\z. zx) x) (x y z)
- The Y operator is not the only fixed-point combinator in the lambda
calculus (there are an
*infinite*number of them). Turing's theta operator is defined by the expression
`A A` where`A` stands for the exression`\x. \y. y (x x y)` . Show that the theta operator is a fixed point combinator. - Define a data type for lambda calculus expressions in Haskell and implement the substitution operation! It is only necessary to deal with the case that the variable is substituted for a closed expression. If you are ambitous, you should test for closedness before applying the substitution. Show with some examples that your program works. Hint.
Bengt Nordstrom
Last modified: Wed Oct 29 10:02:44 KST 2003 |