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}