Functional Programming and Type Theory ChungAng University, Fall 2003

Homework in Lambda Calculus

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.
Good luck!
Bengt Nordstrom

Last modified: Wed Oct 29 10:02:44 KST 2003