Combinator engine: answers to exercises

PURPOSE: Answers to the exercises found in Combinator Engine

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 x

To prove:

    T x f = C I x f = f x

    C I x f = I f x
             = f x

To 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 x

To 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 x

To prove:

    S p I = W p

    S p I x = p x { I x }
            = p x x
            = W p x

To prove:

    S p {K q} = C p q

    S p {K q} x = p x {K q x}
                = p x q
                = C p q x

The remaining two identities were already proven in exercise 2.

Exercise 4. Explain why

    n { K false } true

tests for zero.

    n { K false } true

is true if n is zero. Otherwise, it's

    K false { K false { ... true } ... }
    \------  ------/
           \/
         n times

But, since

    K false x = false

for 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}