Deadline: Oct 30

1. Evaluate the following lambda calculus expressions to normal form. If no normal form exists, explain why.
   1. (\x. \y. x x y) (\x. x x)
   2. (\x. \y. x (x y)) (\x. x x)
   3. (\x. (\z. zx) x) (x y z)
2. 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.
3. 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.