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
We have seen that the primitive combinators S and K can define all other combinators such as
C, I, B, etc. Thus, it should be possible to prove it using these two primitive combinators.
Show the completeness of the S-K basis by answering to the following question.
Question: Calculate the given combinatorial expressions using the definitions:
Sxyz:=xz(yz)
Kxy:=x
Ix:=x
(1) S K K x
(2) S (K S) K x y z
(3) S (K (S I)) K x y
(4) S (K (S I)) (S (K K ) I) x y
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 following lambda terms into a combinator using the T[] definition:
(5) λx.λy.(yx)
(6) λx.λy.(xy)