Ackermann function in terms of higher order recursion

Wikipedia provides a higher-order definition of Ackermann function. First it gives the normal recursive definition \begin{equation*} A(m,n)=\left\{ \begin{array}{ll} n+1 & \text{if $m=0$} \\ A(m-1,1) & \text{if $m>0$ and $n=0$} \\ A(m-1,A(m,n-1)) & \text{if $m>0$ and $n>0$.} \end{array}\right. \end{equation*} After which it provides higher-order formulas \begin{equation*} \begin{array}{lcl} A(0)&=&S\\ A(m+1)&=&I(A(m)) \end{array} \end{equation*} where $S$ is successor function and I is defined as \begin{equation*} \begin{array}{lcl} I(f)(0)&=&f(1)\\ I(f)(n+1)&=&f(I(f)(n)). \end{array} \end{equation*}

I don't follow the construction. I computed some small values of $m$ and it seems correct compared to the table provided in Wikipedia, but how would one prove these two definitions equal?

-
Did you try induction? –  Julian Kuelshammer Jan 17 '13 at 9:10
@JulianKuelshammer I can't get off the ground. The higher-order construction seems somewhat "unreachable" for the normal tools I would deploy here. I did rewrite and study the function in terms of Knuth up-arrow notation and will try if I figure a way to pull the proof of with it. The main goal is to understand the higher-order induction better (to get a new tool to work with). –  rank Jan 17 '13 at 10:08

The quoted definitions will be awkward to work with, since the first definition uses $A$ for a binary function while the second uses $A$ for a unary, function-valued function (the "curried" form of the first $A$). I suggest using different symbols; for example, write $B$ instead of $A$ in the higher-order version. Then what you want to prove is that $A(m,n)=B(m)(n)$. This should be doable by a double induction; start doing an induction on $m$, and within its induction step you'll do an auxiliary induction on $n$. An additional awkwardness arises from the fact that the first definition writes the induction step as going from $m-1$ to $m$ while the second goes from $m$ to $m+1$; I'd suggest changing variables in one of the two to make them match up.