if 0 {[Richard Suchenwirth] 2004-10-24 - Reading 
   * John McCarthy: A basis for a mathematical theory of computation, in: Computer Programming and Formal Systems. P.Braffort, D.Hirschberg (ed.), Amsterdam:North Holland 1963, 
I was challenged to play with [recursive functions], especially with
the theorem that "any partial recursive function (Kleene) on the
non-negative integers is in C{F} where F contains only the successor
function and the predicate equality". C{F} is the class of functions
computable in terms of the given base functions F.

This goes in the direction of [If we had no expr]. What interested me is
that two functions should be enough to derive all arithmetics, so I
tried it in Tcl. succ is easily implemented as
 proc succ x {incr x}
and equality of integers in canonical form can, without using [expr], be
had as
 proc eq {m n} {string equal $m $n}
Most important is how to compose these functions. McCarthy advocates
"conditional expressions", alternating sequences of {condition} {result}
like
 A B C D ...
which can in Tcl (and many other languages) be implemented as
 if $A then $B elseif $C then $D ...
or more compactly with [expr]'s ?: ternary operator:
 $A? $B: $C? $D: ...
I decided to use [expr] in these experiments only for the ?: operator
- the others shall be recreated from the two "axioms". Here's the [func] wrapper
that hides the use of [expr]:}
 proc func {name argl body} {proc $name $argl [list expr $body]}
if 0 {and, as we'll need some testing interweaved with func definitions,
here's a tiny multi-case tester:}
 proc test args {
    foreach {case expected} $args {
        catch {uplevel 1 $case} res
        if {$res != $expected} {error "$case->$res, expected $expected"}
    }
 }
if 0 {So, let's go. Following McCarthy's notation, I use shorter symbolic names for
the two basic functions:}
 proc '  x    {incr x}
 test {' 0} 1 {' 42} 43 
 proc = {m n} {string equal $m $n}
 test {= 0 0} 1 {= 0 42} 0 {= 42 42} 1
if 0 {The partial converse of the successor function is the
predecessor ("the non-negative integer before"), where the auxiliary function
pred2 uses recursion - it calls itself (as most of the following will). The next
definitions are a mechanical transcription to Tcl of McCarthy's:}
 func pred   n    {[pred2 $n 0]}
 func pred2 {n m} {[= [' $m] $n]? $m: [pred2 $n [' $m]]}
 test {pred 42} 41 {pred 1} 0
#-- This allows us to define the sum:
 func + {m n} {[= $n 0]? $m: [+ [' $m] [pred $n]]}
 test {+ 3 4} 7
#-- the product
 func * {m n} {[= $n 0]? 0: [+ $m [* $m [pred $n]]]}
 test {* 3 4} 12
#-- the difference (defined only for m >= n)
 func - {m n} {[= $n 0]? $m: [- [pred $m] [pred $n]]}
 test {- 12 7} 5 {- 1 1} 0 {- 0 0} 0
#-- the inequality predicate <=
 func <= {m n} {[= $m 0]? 1: [= $n 0]? 0: [<= [pred $m] [pred $n]]}
 test {<= 1 2} 1 {<= 2 2} 1 {<= 3 2} 0
#-- leading to the strict inequality <
 func < {m n} {[= $m $n]? 0: [<= $m $n]}
 test {< 1 2} 1 {< 2 2} 0 {< 3 2} 0
#-- Integer division goes like this:
 func / {m n} {[< $m $n]? 0: [' [/ [- $m $n] $n]]}
 test {/ 1 2} 0 {/ 2 2} 1 {/ 3 2} 1 {/ 42 2} 21
#-- Integer division remainder (% in expr)
 func rem {m n} {[< $m $n]? $m: [rem [- $m $n] $n]}
 test {rem 1 2} 1 {rem 2 2} 0 {rem 3 2} 1
#-- Divisibility of a number n by a number m
 func | {m n} {[= $n 0]? 1: [< $n $m]? 0: [| $m [- $n $m]]}
 test {| 2 42} 1 {| 2 43} 0 {| 2 3} 0
if 0 {Primeness of a number uses another auxiliary function. Here I
found a bug in McCarthy's paper - the order of m and n was reversed in prime2:}
 func prime   n    {[= $n 0]? 0: [= $n 1]? 0: [prime2 $n 2]}
 func prime2 {m n} {[= $m $n]? 1: [| $n $m]? 0: [prime2 $m [' $n]]}
 test {prime 2} 1 {prime 3} 1 {prime 4} 0 {prime 5} 1 {prime 6} 0 {prime 7} 1
#-- Greatest common denominator, according to Euclid's algorithm:
 func gcd {m n} {[<= $n $m]?        [gcd $n $m]:
                 [= [rem $n $m] 0]? $m:
                                    [gcd [rem $n $m] $m]}
 test {gcd 12 24} 12 {gcd 12 18} 6 {gcd 17 19} 1
if 0 {McCarthy's argument culminated in defining Euler's ''phi'' function
(phi(n) being the number of numbers less than n and relatively prime to
n), but as I didn't have a reference implementation, I stopped as this
point. In any case, his argument that functions composed only of
''succ'' and ''eq'' can do a helluva lot, has been confirmed in Tcl :-)
----
[Arts and crafts of Tcl-Tk programming]
}