Understanding recursion over higher order types

124 Views Asked by At

I'm reading this answer which defines Ackermann function via higher order recursion https://mathoverflow.net/a/47098

First we define an iteration function $g\colon\mathbb{N}\times\mathbb{N^N}\to\mathbb{N^N}$ : \begin{array}{l} g(0,f) = i \\ g(n+1, f) = f\circ g(n, f) \end{array}

where $i$ is identity function. Then we define a version of the Ackermann function as a function $A\colon\mathbb{N}\to\mathbb{N^N}$, by: \begin{array}{l} A(0) = S \\ A(n+1) = g(n, A(n)) \end{array} where $S$ is successor function.

Now, reading the definitions, I get \begin{array}{l} A(0) = S \\ A(1) = g(0,A(0)) = g(0,S) = i \\ A(2) = g(1,A(1)) = g(1,i) = i\circ g(0,i) = i\circ i = i \\ A(3) = g(2,A(2)) = g(2,i) = \dots = i \end{array}

Clearly I'm not interpreting this correctly. How the recursion over higher order types works? Working with the two-parameter version of Ackermann function, I take we should get $A(0,n) = n+1$, $A(1,n) = n+2$, $A(2,n) = 2n+3$ etc., but I'm not able to get these with the above definitions. Should we have/should I read in the definition of $A$ the recursion as something like $A(n+1) = g(A(n),A(n))$?

1

There are 1 best solutions below

1
On BEST ANSWER

The cited definition is wrong, as you've observed. To get $A(m + 1)$, we want to apply $A(m)$ repeatedly to 1. Redefine $g : \mathbb{N}^\mathbb{N} \to \mathbb{N}^\mathbb{N}$ as follows:

$$ \begin{align} g(f)(0) &= f(1)\\ g(f)(n + 1) &= f(g(f)(n))\\ \end{align} $$

Or more simply, $g(f)(n) = f^{n + 1}(1)$.

Then the Ackermann function can be defined recursively as

$$ \begin{align} A(0) &= S\\ A(m + 1) &= g(A(m))\\ \end{align} $$

For example, $A(1)(n) = g(A(0))(n) = g(S)(n) = S^{n + 1}(1) = n + 2$. So $A(1) = S^2$. $A(2)(n) = g(A(1))(n) = g(S^2)(n) = (S^2)^{n + 1}(1) = 2n + 3$.