[KBK] - After burning myself on [hot curry], I started wasting ''entirely'' too much time on an engine that builds up recursive function theory from a minimalist set of primitives.

In this page, we'll be developing an implementation of the factorial function in a language with:
   * no if statement.
   * no while loops.  In fact, no control structures at all, except as shown below.
   * no named variables.
   * no named user functions (Well, we'll use named functions for shorthand, but we could expand their definitions recursively.

The only control structures are [[S]] and [K], defined as
    S a b c = a c { b c }
    K a b   = a

And we have a few additional functions:

   addition: + a b
   subtraction: - a b
   multiplication: * a b
   division: / a b
   test for zero: zero? a
         This last function returns K if a is zero, and K { S K K } otherwise.

And that's all.  We'll allow for simple expansion of named functions, so that we can write

    define I S K K

but that's just shorthand, we could simply spell things out everywhere.
----
(4 December 2002) [KBK] improved the optimizer and added a little bit more discussion.

# In order to keep my sanity, I found myself needing to trace what the engine did, so my source file begins with

 set tracemax 100000
 set tracen 0
 proc trace args {
     global tracen tracemax
     if { [incr tracen] > $tracemax } exit
     puts [format %*s%s [info level] {} $args]
 }
 proc trace args {}

# The fundamental problem with [hot curry] is that eager evaluation gets in the way of searching for fixed points. Hence we do our own ''lazy'' evaluator.  The evaluator can be extremely simple, since every function that it recognizes has a single argument!

 proc lazyEval args {
     # if we've got a list as the first arg, flatten it.
     set f [lindex $args 0]
     while { 1 } {
	 trace evaluating $args
	 if { [llength $f] > 1 || [string match {{*}} $f] } {
	     trace expanding $f
	     set args [eval [list lreplace $args 0 0] $f]
	     set f [lindex $args 0]
	 } elseif { [llength $args] > 1 } {
	     set f [lindex $args 0]
	     set g [lindex $args 1]
	     trace applying $f to $g
	     set result [$f $g]
	     trace replacing $f $g -> $result
	     set args [eval [list lreplace $args 0 1] $result]
	     set f [lindex $args 0]
	 } else {
	     break
	 }
     }
     # return the single arg
     trace result $args
     return $args
 }

# It's convenient to have anonymous lambdas.  Alas, there isn't any graceful way to implement [lambda in Tcl].  Here's a hack that leaks memory.

 variable lambdaIndex 0
 proc lambda { x y } {
    variable lambdaIndex
    variable lambdaCache
    set key [list $x $y]
    if { ! [info exists lambdaCache($key)] } {
	set pname lambda[incr lambdaIndex]
	set lambdaCache($key) $pname
	proc $pname $x $y
    }
    return $lambdaCache($key)
 }

# We curry the ''K'' and ''S'' combinators by hand.  Note that some special handling is needed because the arguments are unevaluated - we are doing ''lazy'' evaluation, after all!

# K x y = x

 proc K x { lambda y "lazyEval $x" }

# S f g x = f x (g x)

 proc S f { lambda g "[list S2 $f] \$g" }
 proc S2 { f g } { lambda x "[list S3 $f $g] \$x" }
 proc S3 { f g x } {
     trace evaluating curried S $f $g $x
     set toEval [list lazyEval $f $x [list $g $x]]
     set result [eval $toEval]
     trace returning $result
     return $result
 }

# Now, if we've done everything right, we should see that S K K is the identity operation.

 puts [lazyEval S K K this-should-pass-unchanged]
 #                    -> prints this-should-pass-through-unchanged

# Let's define lazy, curried, versions of the four arithmetic operators.

 proc + x { lambda y "[list ++ $x] \$y" }
 proc ++ { x y } {
     trace evaluating + $x $y
     set realX [uplevel 1 [list lazyEval $x]]
     set realY [uplevel 1 [list lazyEval $y]]
     set result [expr { $realX + $realY }]
     trace returning $result
     return $result
 }
 proc - x { lambda y "[list -- $x] \$y" }
 proc -- { x y } {
     trace evaluating - $x $y
     set realX [uplevel 1 [list lazyEval $x]]
     set realY [uplevel 1 [list lazyEval $y]]
     set result [expr { $realX - $realY }]
     trace returning $result
     return $result
 }
 proc * x { lambda y "[list ** $x] \$y" }
 proc ** { x y } {
     trace evaluating * $x $y
     set realX [uplevel 1 [list lazyEval $x]]
     set realY [uplevel 1 [list lazyEval $y]]
     set result [expr { $realX * $realY }]
     trace returning $result
     return $result
 }
 proc / x { lambda y "[list // $x] \$y" }
 proc // { x y } {
     trace evaluating / $x $y
     set realX [uplevel 1 [list lazyEval $x]]
     set realY [uplevel 1 [list lazyEval $y]]
     set result [expr { $realX / $realY }]
     trace returning $result
     return $result
 }
 puts [lazyEval + 6 2]
 puts [lazyEval - 6 2]
 puts [lazyEval * 6 2]
 puts [lazyEval / 6 2]
 #                    print 8, 4, 12, and 3 respectively

# We want to be able to define new combinators.  The ''define'' procedure is a little bit of syntactic sugar around [[interp alias]]:

 proc define {key args} {
     trace [list interp alias {} $key {} lazyEval] $args
     eval [list interp alias {} $key {} lazyEval] $args
 }

# OK, now we have enough in hand to define some of the basic combinators.

# The identity function, I x == x

 define I S K K
 puts [lazyEval I this-should-pass-through-unchanged]
 #                    prints this-should-pass-through-unchanged
# ''Exercise 1:'' Try to prove this yourself, it isn't hard.  If you get stuck, see [Combinator engine: answers to exercises]

# The composition operator B f g x = f (g x)

 define B S {K S} K
 puts [lazyEval B {+ 1} {* 2} 3]
 #                    prints 7

# The alternative curry C f x y = f y x
 define C S {B B S} {K K}
 puts [lazyEval C - 5 8]
 #                    prints 3

# Apply a function to a constant  T x f = f x

 define T C I
 puts [lazyEval T 3 {- 10}]
 #                    prints 7

# Duplicate an argument to a function W f x = f x x

 define W C S I
 puts [lazyEval W * 6]
 #                    prints 36

# ''Exercise 2:'' Prove all of these.  If you get stuck, the answers are over in [Combinator engine: answers to exercises].

# While it isn't strictly necessary, it's helpful to have a compiler to abstract free variables from expressions.  Essentially, this is translating the lambda calculus to the algebra of S and K
 #    * Lambda x (f g) => S (Lambda x f) (Lambda x g)
 #    * Lambda x a ==> K a
 #    * Lambda x x ==> I

 proc Lambda { x f } {
     trace abstracting $x from $f
     if { [llength $f] > 1 } {
 	set retval [list S \
			[Lambda $x [lrange $f 0 end-1]] \
			[Lambda $x [lindex $f end]]]
     } elseif { [string equal $f $x] } {
	 set retval I
     } else {
	 set retval [list K $f]
     }
     trace returning $retval
     return [Opt $retval]
 }

# We also apply a few optimizations:
 #    * Redundant brackets are removed
 #    * S (K a) I ==> a
 #    * S (K a) (K b) ==> K (a b)
 #    * S (K a) => B a
 #    * S a (K b) => C a b
# ''Exercise 3:'' Prove that the last four optimizations are correct.  [Combinator engine: answers to exercises]
 proc Opt x {
    trace optimizing $x
    # remove redundant brackets
    if { [string match {{*}} $x] && [llength $x] == 1 } {
	trace removing redundant brackets
	set x [Opt [lindex $x 0]]
    }
    set first [lindex $x 0]
    if { [llength $first] > 1 || [string match {{*}} $first] } {
	trace removing redundant brackets from $first
	set y [Opt $first]
	eval [list lappend y] [lrange $x 1 end]
	set x [Opt $y]
    }
    if { [llength $x] > 1 } {
	trace optimizing subordinate items
	set r [list]
	foreach item $x {
	    lappend r [Opt $item]
	    set x $r
	}
    }
    if { [llength $x] >= 3 && [string equal S [lindex $x 0]] } {
	set first [lindex $x 1]
	set second [lindex $x 2]
	if { [llength $first] == 2 && [string equal K [lindex $first 0]] } {
	    set a [lindex $first 1]
	    if { [string equal I [lindex $second 0]] } {
		set r [lreplace $x 0 2 $a]
		trace replacing [lrange $x 0 2] with $a
		set x [Opt $r]
	    } elseif { [llength $second] == 2
		       && [string equal K [lindex $second 0]] } {
		set b [lindex $second 1]
		set r [lreplace $x 0 2 K [list $a $b]]
		trace replacing [lrange $x 0 2] with [list K [list $a $b]]
		set x [Opt $r]
	    } else {
		set r [lreplace $x 0 2 B $a $second]
		trace replacing [lrange $x 0 2] with [list B $a $second]
		set x [Opt $r]
	    }
	} elseif { [llength $second]== 2
		   && [string equal K [lindex $second 0]] } {
	    set q [lindex $second 1]
	    set r [lreplace $x 0 2 C $first $q]
	    trace replacing [lrange $x 0 2] with [list C $first $q]
	    set x [Opt $r]
	}
    } elseif { [llength $x] == 2 && [string equal S [lindex $x 0]] } {
	set first [lindex $x 1]
	if { [llength $first] == 2 && [string equal K [lindex $first 0]] } {
	    set p [lindex $first 1]
	    trace replacing $x with [list B $p]
	    set x [Opt [list B $p]]
	}
    }
    trace returning $x
    return $x
 }
 
# Our functions dispense with the [[if]] statement; instead, a Boolean value is a combinator with two arguments.  ''true'' evaluates its first argument and discards the second; ''false'' discards the first and evaluates the second. ([If we had no if]).

 define true K
 define false K {S K K}
 proc zero? n {
     trace evaluating [info level 0]
     set realN [uplevel 1 lazyEval $n]
     if { $realN == 0 } {
 	set result true
     } else {
 	set result false
     }
     trace returning $result
     return $result
 }

if 0 {
Proof: Consider:
    zero? 0 a b == K a b == a
    zero? 1 a b == K {S K K} a b
        == S K K b
        == K b {K b}
        == b
}

# We can test this out quickly:

 puts [lazyEval zero? 0 it-is-zero it-isn't-zero]
 #                    prints it-is-zero
 puts [lazyEval zero? 1 it-is-zero it-isn't-zero]
 #                    prints it-isn't-zero

# OK, now things can get interesting.  Let's define Turing's ''fixed point combinator Y''.  The Y combinator searches for a fixed point of a function f, that is, a value of x such that x = f x.  

 define A B {S I} {S I I}
 define Y A A
 set realY {B {S I} {S I I} {B {S I} {S I I}}}

# How does this work?
 # Y f = A A f
 #     = B (S I) (S I I) A F
 #     = (S I) ((S I I) A) f
 #     = (S I) (S I I A) f
 #     = (S I) (I A (I A)) f
 #     = S I (A A) f
 #     = I f ((A A) f)
 #     = f (A A f)
 #     = f (Y f)

# Who cares?  Well, let's come up with a traditional recursive definition for factorial: 
 # f(n) = (zero? n 1 (* n (f (- n 1)))).  
# In other words, "if n is zero, return 1, otherwise return n*f(n-1)."  Make this function accept a second parameter, which is expected to be the function itself.

 set f1 [Opt [Lambda f [Lambda n { zero? n 1 { * n { f { - n 1 } } } }]]]
 puts [list f1 = $f1]
 #                    prints f1 = {B {S {C zero? 1}} {B {S *} {C B {C - 1}}}} 
 set fact1 [linsert $f1 0 define fact1]
 eval $fact1

# Now, let's see what evaluating Y fact1 2 does:
 # Y fact1 2 = fact1 (Y fact1) 2
 #           = (* 2 (fact1 (Y fact1) 1))
 #           = (* 2 (* 1 (fact1 (Y fact1) 0)))
 #           = (* 2 (* 1 1))

# Wow, recursion without explicit function names!  Let's test it out:
 puts "factorial x is the same as [Opt [list $realY $f1 x]]"
 #                    prints a long expression so that you can see that
 #                    there are NO named functions in it anywhere, but
 #                    it's still recursive, and computes the factorial!
 define factorial $realY $f1
 puts [lazyEval factorial 5]
 #                    prints 120

# We can also do an iterative implementation of factorial:
 set f2 [Opt [Lambda f [Lambda n [Lambda t {
     zero? n t { f { - n 1 } { * t n } }
 }]]]]
 puts [list f2 = $f2]
 #                    prints a long expression...
 set f3 $realY; lappend f3 $f2
 puts "factorial x is also the same as [list C $f3 1 x]"
 #                    prints an even longer expression...
 define factorial2 C $f3 1
 puts [lazyEval factorial2 5]
 #                    once again, prints 120.  Who needs a while
 #                    loop, anyway?

# Even multiple recursion is a piece of cake, as we see with the Fibonacci numbers:
 set fib [Opt [Lambda f [Lambda x {
    zero? x 0 {zero? {- x 1} 1 {+ {f {- x 1}} {f {- x 2}}}}
 }]]]
 puts [list fib = $fib]
 set f3 [linsert $realY 0 define fib]
 lappend f3 $fib
 puts $f3
 eval $f3
 puts [lazyEval fib 7]