CS 342 Principles of Programming Languages Homework 6
Homework Solutions: Lambda Calculus
Learning Objectives:
1. Understand evaluation order
2. Understand church encoding
3. Learn to perform β-reduction
Instructions:
• Total points: 47 pt
• Early deadline: Mar 31 (Wed) at 11:59 PM; Regular deadline: Apr 2 (Fri) at 11:59 PM (you can
continue working on the homework till TA starts to grade the homework).
• Submit one pdf file on Canvas under Assignments, Homework 6 submission. You are encouraged to
use latex. But we will accept a scanned copy as well.
Questions:
1. (9 pt) [β-reduction] Perform β-reduction for the following λ expressions.
(a) (3 pt) (((λ(x)(λ(y)(x y)))((λ(a) a) a))((λ(b) b) b))
(b) (3 pt) (((λ(x)(λ(y)(y)))((λ(z) z) a)) b)
(c) (3 pt) (((λ(x)(x x))(λ(y) y)) x)
Sol.
(a) (3pt)
(((λ(x)(λ(y)(x y)))((λ(a) a) a))((λ(b) b) b)) (1)
= (((λ(x)(λ(y)(x y))) a) b) (2)
= (((λ(y)(a y))) b) (3)
= (a b) (4)
(b) (3pt)
(((λ(x)(λ(y)(y)))((λ(z) z) a)) b) (1)
= (((λ(x)(λ(y)(y)))a) b) (2)
= (((λ(x)(λ(y)(y)))a) b) (3)
= (((λ(y)(y))) b) (4)
= b (5)
Spring 2021 page 1 of 2
CS 342 Principles of Programming Languages Homework 6
(c) (3pt)
(((λ(x)(x x))(λ(y) y)) x) (1)
= (((λ(y)y)(λ(y) y)) x) (2)
= ((λ(y) y) x) (3)
= x (4)
2. (4 pt) [Evaluation order] The goal of this problem is to help you understand the evaluation order of
lambda calculus.
In the following, show the steps of β-reduction for the lambda expression using two types of evaluation
orders
((λ(x) p)((λ(y)(y y))(λ(z)(z z))))
Sol.
(a) (3pt)
((λ(x)p)((λ(y)(y y))(λ(z)(z z)))) (1)
= p (2)
(b) (3pt)
((λ(x)p)((λ(y)(y y))(λ(z)(z z)))) (1)
= ((λ(x)p)((λ(z)(z z)) (λ(z)(z z)))) (2)
= ((λ(x)p)((λ(z)(z z)) (λ(z)(z z)))) (3)
= ((λ(x)p)((λ(z)(z z)) (λ(z)(z z)))) (4)
= … (5)
3. (7 pt) [Church Encoding] Encode the following logic Boolean operations using the encoding of true,
false, ite, not and or provided in the lecture.
(a) (3 pt) and a b
(b) (4 pt) a→ b
Sol.
(a) (ite a
(ite b true false)
false
)
(b)
Spring 2021 page 2 of 2
CS 342 Principles of Programming Languages Homework 6
(ite a
(ite b true false )
true
)
4. (16 pt) [Church Encoding and understanding the semantics of lambda expressions] Using zero, one
and two as well as succ, true and false provided in the lecture, answer the following two questions:
(a) (4 pt) What is the result of ((λ(z)((one f) z)) (succ zero)) ?
(b) Suppose we define unknown: (λ(x)(λ(y)(λ(z) z))) and g: (λ(n)((n unknown) true)), what is the
result of:
i. (4 pt) (g zero)
ii. (3 pt) (g one)
iii. (2 pt) (g two)
iv. (3 pt) What mathematical/logical operation is computed by g?
Sol.
(a) (4 pt)
((λ(z)((one f) z)) (succ zero)) =
((λ(z)(((λ(f)(λ(x)(f x))) f) z)) (succ zero)) =
((λ(z)((λ(x)(f x)) z)) (succ zero)) =
((λ(z)(f z)) (succ zero)) =
((λ(z)(f z)) ((λ(n)(λ(f)(λ(x)(f((n f) x))))) zero)) =
((λ(z)(f z)) (λ(f)(λ(x)(f((zero f) x)))))) =
((λ(z)(f z)) (λ(f)(λ(x)(f(((λ(f)(λ(x)x)) f) x)))))) =
((λ(z)(f z)) (λ(f)(λ(x)(f((λ(x)x) x)))))) =
((λ(z)(f z)) (λ(f)(λ(x)(f x))))) =
((λ(z)(f z)) one)) =
(f one)
(b) i. (4 pt)
(g zero) =
((λ(n)((n unknown) true))zero) =
((zero unknown) true) =
(((λ(f)(λ(x)x)) unknown) true) =
((λ(x)x)true) =
true
ii. (3 pt)
(g one) =
((λ(n)((n unknown) true)) one) =
((one unknown) true) =
(((λ(f)(λ(x)(f x))) unknown) true) =
((λ(x)(unknown x)) true) =
Spring 2021 page 3 of 2
CS 342 Principles of Programming Languages Homework 6
((λ(x)((λ(x)(λ(y)(λ(z) z))) x)) true) =
((λ(x)(λ(y)(λ(z) z))) true) =
((λ(x)false) true) =
false
iii. (2 pt)
(g two) =
((λ(n)((n unknown) true)) two) =
((two unknown) true) =
(((λ(f)(λ(x)(f (f x)))) unknown) true) =
((λ(x)(unknown (unknown x))) true) =
(unknown (unknown true)) =
(unknown ((λ(x)(λ(y)(λ(z) z))) true)) =
(unknown (λ(y)(λ(z) z))) =
(unknown false) =
((λ(x)(λ(y)(λ(z) z))) false) =
(λ(y)(λ(z) z)) =
false
iv. (3 pt) The computation performed is: testing if g is 0.
5. (11 pt) Given:
data: (λ(x) (λ(y) (λ(z) ((z x) y))))
op1: (λ(p) (p (λ(x) (λ(y) x))))
op2: (λ(p) (p (λ(x) (λ(y) y))))
true: (λ(x) (λ(y) x))
false: (λ(x) (λ(y) y))
(a) (4 pt) What is the result of (op1 ((data a) b))?
(b) (4 pt) What is the result of (op2 ((data a) b))?
(c) (3 pt) What computation do op1 and op2 perform?
Sol.
((data a) b)) = (((λ(x) (λ(y) (λ(z) ((z x) y)))) a) b) = (λ(z) ((z a) b))
op1: (λ(p) (p (λ(x) (λ(y) x)))) = (λ(p) (p true))
op2: (λ(p) (p (λ(x) (λ(y) y)))) = (λ(p) (p false))
(a) (op1 ((data a) b)) = ((λ(p) (p true))(λ(z) ((z a) b))) =
((λ(z) ((z a) b))true) =
((true a) b) =
(((λ(x) (λ(y) x)) a) b)=
a
Spring 2021 page 4 of 2
CS 342 Principles of Programming Languages Homework 6
(b) (op2 ((data a) b)) = ((λ(p) (p false))(λ(z) ((z a) b))) =
((λ(z) ((z a) b))false) =
((false a) b) =
(((λ(x) (λ(y) y)) a) b)=
b
(c) op1 and op2 return the first and second element respectively.
Spring 2021 page 5 of 2