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
|