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}