Primitive Recursion

The namespace tnoc.primrec allows the definition of primitive recursive functions following pages 241 and onward.

There are only two built-ins - the successor function S(x) = x + 1 and the literal 0. We can define further primitive recursive functions using composition like so:

(primrec grt [x y] (pos (sub x y)))

This function tests if x > y by subtracting y from x and checking if the result is greater than 0. (pos and sub are previously defined.)

Primitive recursion is performed as follows:

(primrec add
         [x 0] x
         [x (S y)] (S (add x y)))

There are always just two cases - the base case and the recursive case. It is mandatory that the recursion take place in the last parameter. This parameter must be of the form 0 for the base case and (S x) for the recursive case. The only exception is the _ symbol, which can be used to denote unused parameters. An example is:

(primrec Z?
         [0] (S 0)
         [_] 0)

Finally, primitive recursive functions are lazy. They don't compute values until needed. This has the effect that

(primrec select
         [x _ 0] x
         [_ y _] y)

doesn't compute its second argument in the base case or its first argument in the recursive case, leading to substantial time savings. Keep in mind however that select always computes the third argument in order to determine whether to apply the base case or recursive case.