An Exercise in Using Primitive Recursion

Albert Y. C. Lai, trebla [at] vex [dot] net

A Peano natural number type and its primitive recursion scheme are defined:

data PN = Z | S PN
prim c f Z = c
prim c f (S n) = f n (prim c f n)

We wish to implement the equality predicate of two Peano natural numbers, and without recursion apart from prim.

To this end, it benefits us greatly to first study how to apply prim symbolically. Many people understand prim by abbreviating g = prim c f to deduce:

g = prim c f
g Z = c
g (S n) = f n (g n)

The converse also holds (proof by induction) and is more important. So:

g Z = c
g (S n) = f n (g n)
g = prim c f

It is important because it lets us first write a function like g — using explicit recursion as we see fit — and then recognize a pattern and convert it to prim. The symbols will do the work.

More specifically on the pattern: if your function looks like:

g Z = c
g (S n) = ... n ... (g n) ... (g n) ... n ...

in the second equation, you look at how you recurse with g n, and how you use n otherwise. Then you can abstract that out into a λ function and rewrite:

g Z = c
g (S n) = (\p r -> ... p ... r ... r ... p ...) n (g n)

(If necessary, choose fresh names instead of p,r to avoid name clashes. If you don't use (g n), or if you don't use n, that's fine, it just means the λ function has unused parameters.)

Then (\p r -> ... p ... r ... r ... p ...) is your f and you can convert to prim:

g = prim c (\p r -> ... p ... r ... r ... p ...)

This symbolic conversion scheme is exactly what we need because we could implement the equality predicate at ease with explicit recursion, but not so at ease with prim.

Now we begin. The equality predicate is pretty obvious with explicit recursion:

equal Z Z = True
equal Z (S n) = False
equal (S m) Z = False
equal (S m) (S n) = equal m n

First I convert the first two equations; in fact I consider equal Z to be one function g, and so I add parentheses to emphasize that it is one single thing:

(equal Z) Z = True
(equal Z) (S n) = False = (\_ _ -> False) n ((equal Z) n)
equal Z = prim True (\_ _ -> False)

Next, I convert the other two equations, considering equal (S m) to be one function g:

(equal (S m)) Z = False
(equal (S m)) (S n) = equal m n

Although there is a recursion to equal, it is not of the right form: g = equal (S m) here, so the right form of recursion g n would be equal (S m) n, but we only have equal m n. So we pretend this is not a recursion for the moment. (It will be dealt with soon anyway.) But then we are using n “otherwise”. So the λ function here is (\p _ -> equal m p). So the conversion is:

(equal (S m)) Z = False
(equal (S m)) (S n) = (\p _ -> equal m p) n ((equal (S m)) n)
equal (S m) = prim False (\p _ -> equal m p)

At this stage we have these new equations:

equal Z = prim True (\_ _ -> False)
equal (S m) = prim False (\p _ -> equal m p)

Now it is equal's turn to be g and be converted. The recursion is also of the right form: we expect g m here, which is equal m, which does occur now. (On the other hand, m does not occur “otherwise”.) So:

equal Z = prim True (\_ _ -> False)
equal (S m) = (\_ r -> prim False (\p _ -> r p)) m (equal m)
equal = prim (prim True (\_ _ -> False)) (\_ r -> prim False (\p _ -> r p))

That is the answer.

I have more Haskell Notes and Examples