Lambda Calculus CMPT 331

Lambda Calculus
CMPT 331

1. Beta-reduce the following expressions to their normal
form
1.a. (λa λy . y a)(z z)
Expression Explanation
(λa λy . y a)(z z) Initial expression
λy . y a [(z z)/a] Substitute (z z) for a
(λy . y (z z)) β reduction
1.b. (λxλy.(x y))(λz.y)
Expression Explanation
(λxλy.(x y))(λz.y) Initial expression
(λxλw.(x w))(λz.y) Rename y in the left function because it is a bound
variable
(λw.(x w)) [(λz.y)/x] Substitute (λz.y) for x
(λw.((λz.y) w)) β reduction
(y) [w/z] Substitute w for z
(λw.y) β reduction
1.c. (λx.(x x))(λy.(y y))
Expression Explanation
(λx.(x x))(λy.(y y)) Initial expression
(x x) [(λy.(y y))/x] Substitute (λy.(y y)) for x
(λy.(y y)) (λy.(y y)) β reduction
(λy.(y y)) (λz.(z z)) Rename y in the right function because it is a
bound variable
(y y) [(λz.(z z))/y] Substitute (λz.(z z)) for y
(λz.(z z)) (λz.(z z)) β reduction. The expression is irreducible and
there is no normal form because a β reduction will
always result in the starting expression.
1
1.d. K x y
Expression Explanation
K x y Initial expression
(λab.a) x y α convert K
(λb.a) [x/a] Substitute x for a
(λb.x) y β reduction
(x) [y/b] Substitute y for b
x β reduction
1.e. S K
Expression Explanation
S K Initial expression
(λadc.a c (d c)) K α convert S
(λdc.a c (d c)) [K/a] Substitute K for a
(λdc.K c (d c)) β reduction
(λdc.((λxy.x) c (d c))) α convert K
(λy.x) [c/x] Substitute c for x
(λdc.((λy.c) (d c)) β reduction
(c) [(d c)/y] Substitute (d c) for y
λdc.c β reduction. This is equivalent to K′
combinator.
1.f. (S K) y y z
Expression Explanation
(S K) y y z Initial expression
(λdc.c) y y z From Problem 1.e
(λc.c) [y/d] Substitute y for d
(λc.c) y z β reduction
(c) [y/c] Substitute y for c
y z β reduction
1.g. K′
y y z
Expression Explanation
K′ y y z Initial expression
(λdc.c) y y z α convert K′
(λc.c) [y/d] Substitute y for d
(λc.c) y z β reduction
(c) [y/c] Substitute y for c
y z β reduction
2
2. What is the normal form of (K S) (K I)?
Expression Explanation
(K S) (K I) Initial expression
((λab.a) S) (K I) α convert first K
(λb.a) [S/a] Substitute S for a
(λb.S) (K I) β reduction
(S) [(K I)/b] Substitute (K I) for b
S β reduction
(λpqr.pr(q r)) α convert S
3. Prove the following equivalencies by reducing each side to
its normal form.
3.a. I = S K K
Expression Explanation
I
?= S K K Initial expression
λx.x ?= S K K α convert I
λx.x ?= (λyx.x) K From Problem 1.e
(λx.x) [K/y] Substitute K for y
λx.x = λx.x β reduction
3.b. S K K = K I I
Expression Explanation
S K K ?= K I I Initial expression
λx.x ?= K I I From Problem 3.a
λx.x ?= (λab.a) I I α convert K
(λb.a) [I/a] Substitute I for a
λx.x ?= (λb.I) I β reduction
(I) [I/b] Substitute I for b
λx.x ?= I β reduction
λx.x = λx.x α convert I
4. Given the definition of Church numerals, what does ( ¯m n¯) do
when m¯ and n¯ are Church numerals?
To determine the output of ( ¯m n¯), I will solve several example problems to determine the pattern for the
outputs. In the work below, the steps for substitution and β reduction are merged into 1 step for brevity.
3
4.a. (¯2 ¯3)
Expression Explanation
(¯2 ¯3) Initial expression
(λfx.(f (f x)))(¯3) Definition of Church numerals
λx.(¯3 (¯3 x)) β reduction of f
λx.(¯3 ((λgy.(g (g (g y)))) x)) Definition of Church numerals
λx.(¯3 λy.(x (x (x y)))) β reduction of g
λx.((λhz.(h (h (h z)))) (λy.(x (x (x y))))) Definition of Church numerals
λx.λz.(A (A (A z))) β reduction of h and let A = λy.(x (x (x y)))
λx.λz.(A (A ((λy.(x (x (x y)))) z))) Expand A
λx.λz.(A (A (x (x (x z))))) β reduction of y
λx.λz.(A ((λy.(x (x (x y)))) (x (x (x z))))) Expand A
λx.λz.(A (x (x (x (x (x (x z))))))) β reduction of y
λx.λz.((λy.(x (x (x y)))) (x (x (x (x (x (x z))))))) Expand A
λx.λz.(x (x (x (x (x (x (x (x (x z))))))))) β reduction of y. This is equal to the Church
numeral ¯9, which is 3
2 or nm.
4.b. (¯3 ¯2)
Based on the result of (¯2 ¯3), I would expect (¯3 ¯2) to be ¯8, which is 2
3.
(¯3 ¯2) Initial expression
((λfx.(f (f (f x)))) ¯2) Definition of Church numerals
λx.(¯2 (¯2 (¯2 x))) β reduction of f
λx.(¯2 (¯2 ((λgy.(g (g y))) x))) Definition of Church numerals
λx.(¯2 (¯2 (λy.(x (x y))))) β reduction of g
λx.(¯2 ((λhz.(h (h z))) (λy.(x (x y))))) Definition of Church numerals
λx.(¯2 (λz.(A (A z)))) β reduction of h and let A = λy.(x (x y))
λx.(¯2 (λz.(A ((λy.(x (x y))) z)))) Expand A
λx.(¯2 (λz.(A (x (x z))))) β reduction of y
λx.(¯2 (λz.((λy.(x (x y))) (x (x z))))) Expand A
λx.(¯2 (λz.(x (x (x (x z)))))) β reduction of y
λx.((λgy.(g (g y))) (λz.(x (x (x (x z)))))) Definition of Church numerals
λx.(λy.(B (B y))) β reduction of g and let B = λz.(x (x (x (x z))))
λx.(λy.(B ((λz.(x (x (x (x z))))) y))) Expand B
λx.(λy.(B (x (x (x (x y)))))) β reduction of z
λx.λy.((λz.(x (x (x (x z))))) ((x (x (x (x y)))))) Expand B
λx.λy.(x (x (x (x (x (x (x (x y)))))))) β reduction of z. This is equal to the Church
numeral ¯8, which is 2
3 or nm.
4.c. (¯1 ¯2)
Since both examples thus far have matched the pattern of nm, I would expect math to not be broken here
as (¯1 ¯2) should equal ¯2.
(¯1 ¯2) Initial expression
((λfx.(f x)) ¯2) Definition of Church numerals
λx.(¯2 x) β reduction of f
λx.((λgy.(g (g y))) x) Definition of Church numerals
λx.(λy.(x (x y))) β reduction of g. This is equal to the Church
numeral ¯2, which is 2
1 or nm.
4
4.d. (¯0 ¯2)
The final check to ensure ( ¯m n¯) is rasing n to the power of m is to make sure that anything raised to the
power of 0 is equal to 1. Thus, I would expect (¯0 ¯2) to equal ¯1.
(¯0 ¯2) Initial expression
((λfx.x) ¯2) Definition of Church numerals
λx.x β reduction of f. There are no further reductions
that can be done as this is the I combinator. Thus,
the pattern of nm is not satisfied when m = 0.
4.e. Final Results
Overall, given 2 Church numerals, m¯ and n¯, the expression ( ¯m n¯) will evaluate as one of the following
expressions based on the value of m. Note: Subscripts for f denote count as they are all representing the
same variable f.
( ¯m n¯) = (
nm = λfx.(f1 (f2 (f3 · · · (fnm−1 (fnm x))· · ·))), m > 0
I = λx.x, m = 0
5