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