G6021: Comparative Programming
Some more exercises on the λ-calculus
1. Insert all the missing parentheses and λ’s into the following abbreviated λ-terms, where
I = λx.x.
• λxy.x
• λxy.xyy
• λxyz.xz(yz)
• λxyz.x(yz)
• λxyz.xzy
• λxy.x(xy)
• λx.xI
• λx.xII
• λx.xIII
• (λxy.y(xxy))(λxy.y(xxy))
• λf.(λx.f(xx))(λx.f(xx))
Answer:
• (λx.(λy.x))
• (λx.(λy.((xy)y)))
• (λx.(λy.(λz.((xz)(yz)))))
• (λx.(λy.(λz.(x(yz)))))
• (λx.(λy.(λz.((xz)y))))
• (λx.(λy.(x(xy))))
• (λx.(x(λx.x)))
• (λx.((x(λx.x))(λx.x)))
• (λx.(((x(λx.x))(λx.x))(λx.x)))
• ((λx.(λy.(y((xx)y))))(λx.(λy.(y((xx)y))))) • (λf.((λx.(f(xx)))(λx.(f(xx)))))
In the above, of course we could have expanded I as λy.y for example to avoid any possible confusion with other occurrences of the variable x.
For fun (!), you can also try to work out the types of these terms. The last two don’t have a type, but the rest do:
• λxy.x:A→B→A
• λxy.xyy:(A→A→B)→A→B
• λxyz.xz(yz):(A→B→C)→(A→B)→A→C • λxyz.x(yz):(B→C)→(A→B)→A→C
• λxyz.xzy:(A→B→C)→B→A→C
• λxy.x(xy):(A→A)→A→A
• λx.xI :((A→A)→B)→B
1
• λx.xII:((A→A)→(B→B)→C)→C
• λx.xIII:((A→A)→(B→B)→(C→C)→D)→D
2. Let I = λx.x, B = λxyz.x(yz), C = λxyz.xzy, T = λxy.x(xy) and Y = (λxy.y(xxy))(λxy.y(xxy)). Reduce the following terms to normal form, if they have one. You do not need to draw a
reduction graph.
• CI
Answer: CI = (λxyz.xzy)I → λyz.Izy → λyz.zy
• C(λx.xII)I Answer:
•Y
Answer:
C(λx.xII)I = (λxyz.xzy)(λx.xII)I → (λyz.(λx.xII)zy)I
→ λz.(λx.xII)zI → λz.zIII
Y = (λxy.y(xxy))(λxy.y(xxy))
→ λy.y((λxy.y(xxy))(λxy.y(xxy))y)
= λy.y(Y y)
Thus, there is no normal form (Y reduces to a term with Y as a subterm). • TBCI
Answer:
TBCI = → →
=
→ → → = → = → = → =α
(λxy.x(xy))BCI (λy.B(By))CI
B(BC)I (λxyz.x(yz))(BC)I (λyz.(BC)(yz))I λz.BC(Iz)
λz.BCz λz.(λxyz.x(yz))Cz λz.(λyz.C(yz))z λz′.(λyz.C(yz))z′ λz′.(λz.C(z′z)) λz′.(λz.(λxyz′′.xz′′y)(z′z)) λz′.(λz.(λyz′′.z′zz′′y)) λwxyz.wxzy
•TI
Answer: T I = (λxy.x(xy))I → λy.I(Iy) →∗ λy.y
•TT
Answer: T T = (λxy.x(xy))T → λy.T (T y) →∗ λx.λy.x(x(x(xy)))
• TTT (Just joking – this takes 42 beta reductions…) Answer: In case you tried it, the normal form is:
λx.λy.x(x(x(x(x(x(x(x(x(x(x(x(x(x(x(xy)))))))))))))))
2