**Exercise 1:**To prove:

S K K x = x S K K x = K x { K x } = x

**Exercise 2:**To prove:

B f g x = S { K S } K f g x = f { g x } S { K S } K f g x = K S f { K f } g x = S { K f } g x = K f x { g x } = f { g x }To prove:

C f x y = S { B B S } { K K } x y = f y x S { B B S } { K K } f x y = B B S f { K K f } x y = B { S f { K K f } } x y = S f { K K f x } y = f y { K K f x y } = f y { K x y } = f y xTo prove:

T x f = C I x f = f x C I x f = I f x = f xTo prove:

W f x = C S I f x = f x x C S I f x = S f I x = f x { I x } = f x xTo prove:

M x = S I I x = x x S I I x = I x { I x } = x { I x } = x x

**Exercise 3:**To prove:

S { K p } = B p S { K p } x y = K p y { x y } = p { x y } = B p x y ⌷To prove:

B p { K q } = K { p q } B p { K q } x = p { K q x } = p q = K { p q } x ⌷To prove:

B p I = p B p I x = p { I x } = p xTo prove:

S p I = W p S p I x = p x { I x } = p x x = W p xTo prove:

S p {K q} = C p q S p {K q} x = p x {K q x} = p x q = C p q xThe remaining two identities were already proven in exercise 2.

**Exercise 4.**Explain why

n { K false } truetests for zero.

n { K false } trueis

*true*if

*n*is zero. Otherwise, it's

K false { K false { ... true } ... } \------ ------/ \/ n timesBut, since

K false x = falsefor all x, the result is false.

**Exercise 5.**We want to compare two Church numerals to see if one is greater than the other.One possible solution is to use Kleene's trick of making downward-counting lists, starting from both numbers. We can then iterate through the two lists in parallel. The one that hits zero first is the smaller.

# Determine which list hits zero first, retirn false if it's the first and # true if it's the second. set lgrtr [lambda lgrtr [lambda list1 [lambda list2 { zero? { hd list1 } false { zero? { hd list2 } true { lgrtr { tl list1 } { tl list2 } } } }]]] puts "lgrtr = $lgrtr" macro lgrtr $lgrtr # Determine which of two Church numerals is the greater by iterating through # countdown lists set grtr [lambda m [lambda n { Y lgrtr { downFrom m } { downFrom n } }]] puts "grtr = $grtr" macro > $grtr

**Exercise 6.**We want to find the greatest common divisor of two Church numerals.We use Euclid's algorithm, and compute the remainder of division by repeated subtraction.Our "greater-than" procedure from Exercise 5 takes more time than I have patience for, so let's make a supercombinator that does it:

curry > { x y } { [expr { ([lazyEval $x] > [lazyEval $y]) ? true : false }] }# Then here is the 'gcd' procedure, in full.

set gcd [lambda gcd [lambda m [lambda n { > n m { gcd n m } { zero? n m { gcd { - m n } n } } }]]] puts "gcd = $gcd" macro gcd $gcd demonstrate {Y gcd 48 78}