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

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

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

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

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

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 :-)

---