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)
(b) (3pt)
(((λ(x)(λ(y)(x y)))((λ(a) a) a))((λ(b) b) b))
= (((λ(x)(λ(y)(x y))) a) b)
= (((λ(y)(a y))) b) = (ab)
(((λ(x)(λ(y)(y)))((λ(z) z) a)) b) (((λ(x)(λ(y)(y)))a) b) (((λ(x)(λ(y)(y)))a) b) (((λ(y)(y))) b)
(1) (2) (3) (4)
(1) (2) (3) (4) (5)
Spring 2021
page 1 of 2
=
=
= =b
CS 342 Principles of Programming Languages (c) (3pt)
Homework 6
3. (7 pt) [Church Encoding] Encode the
false, ite, not and or provided in the lecture.
(a) (3pt)andab (b) (4pt)a→b
Sol.
(a)
(ite a
(b) Spring 2021
page 2 of 2
)
(ite b true false) false
(((λ(x)(x x))(λ(y) y)) x) (((λ(y)y)(λ(y) y)) x) ((λ(y) y) x)
(1) (2) (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
Sol.
(a) (3pt)
(b) (3pt)
((λ(x) p)((λ(y)(y y))(λ(z)(z z))))
((λ(x)p)((λ(y)(y y))(λ(z)(z =p
z)))) (1) (2)
z)))) (1) z)))) (2) z)))) (3) z)))) (4)
(5)
= = = =
((λ(x)p)((λ(y)(y y))(λ(z)(z ((λ(x)p)((λ(z)(z z)) (λ(z)(z ((λ(x)p)((λ(z)(z z)) (λ(z)(z ((λ(x)p)((λ(z)(z z)) (λ(z)(z …
following logic Boolean operations using the encoding of true,
CS 342 Principles of Programming Languages Homework 6
(ite a
true
(ite b true false )
)
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.
ii.
(4 pt)
(g zero) =
((λ(n)((n unknown) true))zero) = ((zero unknown) true) =
(((λ(f )(λ(x)x)) unknown) true) = ((λ(x)x)true) =
true
(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)f alse) true) =
f alse
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 f alse) =
((λ(x)(λ(y)(λ(z) z))) f alse) =
(λ(y)(λ(z) z)) =
f alse
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 f alse))(λ(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