Primitive recursion

Primitive recursion

May 11, 2020
type theory
primitive recursion

Finding a primitive recursion representation of a given function \(f\) can be reduced to finding functions \(g, h, k\) such that

  1. \(f(m,0) = g(m)\)
  2. \(f(m,S(n)) = k(h(m,n), f(m,n))\)

where \(S: \mathbf{N} \rightarrow \mathbf{N}\) is a successor function turning a natural number into its successor (1 maps to 2, 2 maps to 3, and so on).

The sought functions should be a composition of one of the following primitive functions:

  1. \(Zero: \mathbf{N} \rightarrow \mathbf{N}, \quad Zero(n) = 0 \)
  2. \(S: \mathbf{N} \rightarrow \mathbf{N}, \quad S(n) = n+1 \)
  3. \(\pi_i: \mathbf{N^d} \rightarrow \mathbf{N}, \quad \pi_i ((n_1, n_2, \dots, n_d)) = n_i \)

which are called zero, successor, and projection (on i) respectively.

How does this relate to our informal definition of recursion? Let’s take a look at an addition function \(add: \mathbf{N} \times \mathbf{N} \rightarrow \mathbf{N} \) that simply adds two natural numbers. Since \(m + (n + 1) = (m + n) + 1\) we can define addition recursively as \(add(m, S(n)) = S(add(m, n))\) .

To get the definition match up with the definition above, note that \(add(n, 0) = n = id_{\mathbf{N}}\) is the identity function on \(\mathbf{N}\) . That gives us our function \(g = id_{\mathbf{N}}\)

Since we’re trying to extract the second part of the pair in (2) in the definition of the recursive function, our function \(k\) should be something related to the projection operation and successor. The only sensible to combine functions so far is to compose them, so let \(k = S \circ \pi_2\) . We don’t care about \(h\) since the projection ignores it, but it still has to be a valid function. We can use \(h = Z \circ \pi_1\) as a valid function (since we gotta make sure it takes 2 arguments).

Putting it all together, we get

  1. \(add(m,0) = id(m)\)
  2. \(add(m,S(n)) = (S \circ \pi_2)((Zero \circ \pi_1)(m,n), add(m,n))\)

Which now looks like the primitive recursive definition