5.5 Primitive Recursive Functions
In the previous section, we leaned about the primitive recursive function called the "successor", one that was used by Peano in his axioms. There are other primitive recursive functions as well, and these are usually given as axioms (i.e., without proof):
- the "zero function"
- the "projection function"
- "identity function"
These combined with the Peano axioms allow us to define other primitive recursive functions.
In the literature, the definition for Peano addition is done in the following manner:
a + 0 = a, a + S(b) = S(a + b)
S is the successor function defined in the previous section.
First we have an identity function: any number that has zero added to it yields the result of the number itself.
Secondly, a number, when added with the successor of another number is equal to the successor of the two numbers combined. Let's take a look at an example:
- The number 0, when applied to the successor function yields 1 (
S(0) = 1)
a + S(0) = a + 1
- By Peano's definition of addition then, we have
a + 1 = S(a + 0)
- Which then gives
a + 1 = S(a)
In other words, the successor of
a + 1.
These rules for addition are sometimes given in the following pseudo code:
add(0, x) = x add(succ(n), x) = succ(add(n, x))
In LFE, we'd like to maintain symmetry with this. We could try to construct a function that had both definitions as pattern arguments, thus alleviating the need for two function definitions. However, to perfectly map the pseudo code to LFE, we'd have to put a function call in our pattern... and that's not possible.
If, though, we do a little algebraic juggling, we can work around this. In our
pseudo code we have two parameters:
x. If we apply a
"predecessor" function to
succ(n), we'll just have
n -- which would
do nicely for a matched function argument in LFE. But we'll also need to apply
this predecessor function to the
n on the other side of the equation.
Let's create such a "predecessor" function:
Now, we can recast the canonical form above using the workaround of the
predecessor primitive recursive function, allowing us to use one function
to define Peano's addition axiom:
All of this may seem rather absurd, given what we do in every-day programming. Remember, though: the verbosity of these axioms and their derived definitions serves to explicitly show that no assumptions are being made. With a foundation of no assumption, we can be certain that each brick we lay on top of this sound (if possibly baroque) basis will be unshakable (baring the random proof by Gödel, of course).
Next up, let's take a look at subtraction:
sub(0, x) = x sub(pred(n), x) = pred(sub(n, x))
Similar to addition above, we make some adjustments for the convenience of pattern matching:
Due to the manner in which we have defined our functions, the usual usage is
reversed for our
subtract function. The first operand is not the number
that is being subtracted from, but rather the number that is being subtracted.
We can see this in action if we put our definitions in a file called
prf.lfe (named for "primitive recursive functions") and
slurp it in
the LFE REPL:
The last one of these that we will look at is multiplication, and then we'll move on to something a little more complicated :-)
mult(0, x) = 0 mult(succ(n), x) = x + (x * n)
Again, using our pattern workaround: