Understanding recursion over higher order types

ackermann-functioncomputabilitylogicrecursiontype-theory

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))$?

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$.

Related Question