Spring 2012 IA165 Combinatory Logic for Computational Semantics by Juyeon Kang
Classwork N°.2
due to 2nd March 2012
1. Combinatory base : S and K
Proof of the completeness of the S-K basis
Question: Calculate the following combinatorial expressions using the rules:
Sxyz:=xz(yz)
Kxy:=x
Ix:=x
(1) S K K x
=Kx(Kx)
=x
(2) S (K S) K x y z
=KSx(Kx)yz
=S(Kx)yz
=Kxz(yz)
=x(yz)
(3) S (K (S I)) K x y
=K(S I) x (K x) y
=S I (K x)y
=I y (K x y)
=y (K x y)
=(y x)
(4) S (K (S I)) (S (K K ) I) x y
Spring 2012 IA165 Combinatory Logic for Computational Semantics by Juyeon Kang
=K(SI)x(S(KK)I x)y
=S I (S (K K)) I x)y
=I y (S (K K) I x y)
=y (S (K K) I x y
=y (K K x (I x) y)
=y (K(I x)y)
=y (I x)
=(y x)
2. Abstraction algorithm
T[] may be defined as follows:
1'| T[v] => v
2'| T[(E1 E2)] => (T(E1) T(E2))
3'| T[λx.E] => (K T[E])
4'| T[λx.x] => I
5'| T[λx.λy.E] => T[λx.T [λy.E]]
6'| T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2])
Question: Convert the lambda term λx.λy.(yx) to a combinator:
a)
T[λx.λy.(yx)]
=T[λx.T[λy.(yx)] (by 5)
=T[λx.(S T[λy.(y)] T[λy.x])] (by 6)
=T[λx.(S I T[λy.x])] (by 4)
=T[λx.(S I (Kx))] (by 3 and 1)
=(S T[λx.(S I)] T[ λx. (Kx))] (by 6)
=(S K (S I)] T[ λx. (Kx))] (by 3)
=(S K (S I)) (S T[ λx. K] T[λx.x])) (by 6)
Spring 2012 IA165 Combinatory Logic for Computational Semantics by Juyeon Kang
=(S K (S I)) (S (K K) T[λx.x])) (by 3)
=(S K (S I)) (S (K K) I )) (by 4)
b) λx.λy.(xy)
=T[λx.λy.(xy)]
=T[λx.T[λy.(xy)]] (by 5)
=T[λx.(S T [λy.x] T [λy.y])] (by 6)
=T[λx.(S T [λy.x] I)] (by 4)
=K S (T[λy.x] I) (by 3)
=K S K x I (by 3)
=K S x (by e.-K)
=S (by e.-K)