Robert Zieba

28 Jan 2019

Natural Numbers and Primitve Recursive Functions in Haskell

Since the mathematics of computer science was developed and formalized in the early decades of the 1900s, three different computational models have risen to prominence and have been show to be equally powerful. These models are Turing machines, Lambda calculus and μ-recursive functions. A Turing machine models computations by the action of a machine manipulating symbols on a tape and is probably the most widely know model for computations. Lambda calculus models computation through the composition and application of anonymous functions and is best known as the foundation for functional programming languages. μ-Recursive functions are, as implied by the name, based on recursive functions. More particularly, they are partial functions whose domains are tuples of natural numbers and return a single natural number. In particular, this article is going to focus on a proper subset of the μ-recursive functions known as the primitive recursive functions. These functions can be simple and elegantly represented in a functional programming language like Haskell. This article will begin with a brief overview of Peano axioms and the natural numbers.

Natural Numbers and Peano Axioms

The natural numbers are the integers \(( 0, 1, 2, …, \) written as \( \mathbb{N} \) . Some definitions do not include zero as a natural number, but for this article it is considered to be one. In 1889, Giuseppe Peano published a list of axioms that formalized the natural numbers which are now known as the Peano axioms. Peano included axioms for things like equality, but I’m going to consider those to be obvious and focus instead on the meat of the axioms which defines the natural numbers as such: 0 is a natural number, the successor of a natural number (written as S(x)) is a natural number. These two simple statements are powerful enough to define the natural numbers. 0 provides a base that we can build upon to generate the natural numbers like so: \( 0,S(0),S(S(0)),… \) and so on. From this point of view, numerals like 1 or 2 are just convenient labels for \( S(0) \) and \( S(S(0))\).

Arithmetic on Natural Numbers

With the above construction of the natural numbers we can define some simple arithmetic, starting with addition.

Addition

$$ x + 0 =x $$ $$ x + S(y) = S(x + y) $$

These two axioms are all that are required to define arithmetic on the natural numbers. If the seconds statement seems confusing, it can be written in the normal language of arithmetic as

$$ x + (y + 1) = (x + y) + 1 $$

To demonstrate, here’s the process for computing \( 2 + 2 \)

$$ S(S(0)) + S(S(0)) $$ $$ =S(S(S(0))+S(0))S(S(0)) + S(0) $$ $$ =S(S(S(0))+0)S(S(0)) + 0 $$ $$ =S(S(0))+S(S(0)) + S(0) $$ $$ = S(S(S(0)) + 0) $$ $$ =S(S(S(0)))+S(S(0)) + S(S(0)) $$ $$ =S(S(S(0))+S(0))=S(S(S(S(0)))) $$

Our two original statements allow us to define a process where, given two numbers x and y, we apply the successor function y times to x. In the language of normal arithmetic, we are doing 2+2=(2+1)+1=(((2+0)+1)+1). Also notice that we have x+0=x, but not 0+x=x. The latter is unnecessary and follows from our original axioms because 0+x

is the successor function applied to 0, x times, which is just x.

Multiplication

We can define multiplication through addition

$$ x \cdot 0 = 0 $$ $$ x \cdot S(y) = x \cdot y + x $$

Subtraction

Subtraction is interesting. Since we are working with the natural numbers, we cannot fully define subtraction as is. Instead, we define a limited subtraction function such that

$$ 0 − x = 0 $$

To do this we’ll need an auxiliary function, simply called the predecessor function, defined as:

$$ pred(0) = 0 $$ $$ pred(S(y)) = y $$

Now, in analogy with addition, we can defined limited subtraction as:

$$ x − 0 = 0 $$ $$ x − S(y) = pred(x − y) $$

Exponentiation

With multiplication we can define exponentiation and factorials.

$$ x^0 = 1 $$ $$ x^S(y) = x\cdot x^y $$

$$ 0! = 1 $$ $$ S(x)! = S(x)\cdot(x!) $$

Primitive Recursive Functions and Haskell

The functions that we defined in the previous section were defined through the use of pattern matching, recursion, and auxiliary functions with these properties. They are also functions from tuples of natural numbers to the natural numbers and are total functions. These functions are primitive recursive functions. The actual definitions of primitive recursive functions are slightly more strict than this, but not by much and our current works provide a clear and intuitive understanding. The definitions of our functions are straightforward to implement in Haskell. To begin, we’ll implement natural numbers in a module called Primitive.

module Primitive where

data N = Zero | Succ N

We'll need some functions to convert between our natural numbers and the integers provided by Haskell as well as a show instance for displaying our numbers in a nice way.

```haskell
toIntegral :: (Integral a) => N -> a
toIntegral Zero = 0
toIntegral (Succ n) = 1 + toIntegral n

fromIntegral :: (Integral a) => a -> Maybe N
fromIntegral i = if i < 0 then Nothing else Just . fromPos $ i 
    where
    fromPos x
        | x < 0 = undefined
        | x == 0 = Zero
        | otherwise = Succ $ fromPos (x - 1)

instance Show N where
    show = show . toIntegral

Now we can get to work on our actual functions. While the Num typeclass doesn’t require it, implementations of it have specific relations between the functions that aren’t a good match for our natural number type so we cannot use the typical function names of +, - and *.

infixl 6 +:
(+:) :: N -> N -> N
(+:) x Zero = x
(+:) x (Succ y) = Succ (x +: y)

infixl 7 *:
(*:) :: N -> N -> N
(*:) x Zero = Zero
(*:) x (Succ y) = x *: y +: x

infixr 8 ^:
(^:) :: N -> N -> N
(^:) x Zero = Succ Zero
(^:) x (Succ y) = x ^: y *: x

pred :: N -> N
pred Zero = Zero
pred (Succ y) = y

infixl 6 -:
(-:) :: N -> N -> N
(-:) x Zero = x
(-:) x (Succ y) = Primitive.pred $ x -: y

factorial :: N -> N
factorial Zero = Succ Zero
factorial y@(Succ x) = y *: (factorial x)

Now we can fire up GHCi

>let (Just a) = Primitive.fromIntegral 5
>let (Just b) = Primitive.fromIntegral 6

>:i a
a :: N

>:i b
b :: N

>a -: b
0
>b -: a
1

>a +: b
11

>a *: b
30

>a ^: b
15625

>factorial a
120

Complete code on Github

Further thoughts

As mentioned in the subtraction section, we don’t have negative numbers since our functions only operate on natural numbers. So how can μ-recursive functions be Turing complete? The answer is that we can encode negative numbers as natural numbers using a Gödel numbering. In fact, we can encode all sorts of data this way, ensuring that μ-recursive functions can operate on it.