Functional Programming and Type Theory ChungAng University, Fall 2003 Homework in Lambda Calculus Deadline: Oct 30 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. Good luck! Bengt Nordstrom Last modified: Wed Oct 29 10:02:44 KST 2003