# 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))
```