CS 440: Programming Languages Assignment: Lambda Calculus
CS 440: Programming Languages
Assignment: Lambda Calculus
Logistics and Submission
Please submit your solutions as a PDF (typed or neatly handwritten!) on Blackboard by the due date. Abstract syntax trees
For each of the following lambda calculus expressions, (a) draw the corresponding abstract syntax tree – following the conventions used in lecture, and (b) circle all the free variables in the AST. (5 points each)
1. λx.x λz.z x
2. (λx.y) (λy.x)
3. (λa.λb.a b) (λx.x x) (λy.b a)
Normal form
For each of the following lambda calculus expressions, (a) indicate whether applicative-order evaluation will eventually find normal form, and (b) if normal form can be reached via either applicative- or normal-order evaluation, show all the steps (β/η-reductions or α-conversions) that lead to it, and normal form itself. If (b) is not possible, show at least three reductions and explain why further normalization is not possible. (5 points each)
4. (λx.λw.w x) w λz.y z
5. (λx.y) ((λw.w w w) (λy.y y y))
6. (λx.x y) (λw.w w)
7. (λx.λy.x y x) (λw.w) (λz.z z)
1
Alternative numbers
As alternatives to the Church numerals discussed in class, consider the following definitions:
TRUE ≡ λx.λy.x FALSE ≡ λx.λy.y
0 ≡ λx.x
INC ≡ λn.λx.(x FALSE) n
1 ≡ INC 0 2 ≡ INC 1
.
8. Based on the definitions above, define the DEC (decrement) function, such that DEC (INC n) ≡ n,
and demonstrate — by showing the necessary reductions — that DEC (DEC 2) ≡ 0. (5 points)
9. Define the IS ZERO function, which should evaluate to TRUE when called on 0 and FALSE otherwise. (5 points)
2
