I'm reading Recursive Functions at Stanford Encyclopedia of Philosophy (section 1.4). The following paragraph defines function β which is then used to define variant of Ackermann-Péter function:
What exactly is the type of Iter? The base case Iter(ϕ, 0) suggests it's (N → N) → N → (N → N), but the inductive step has type (N → N) → N → N.
Assuming it's the former and Iter just composes ϕ with itself, the next paragraph doesn't make sense to me because Iter should have return type N → N, while β should be N → (N → N), so you cannot compose β with itself.
What am I misunderstanding? Thanks.
Update: I've checked the Wikipedia's article on Ackermann function and it turns out that the correct defintion is as follows:
$$β(0) = S$$ $$β(x + 1) = Iter(β(x))$$
where:
$$Iter(ϕ)(0) = ϕ(1)$$ $$Iter(ϕ)(x + 1) = ϕ(Iter(ϕ)(n))$$
You're not misunderstanding, there are a few errors in the text. Your first type signature is right, and the "step" would be more clearly written with a $\circ$ rather than brackets, i.e. $\operatorname{iter}(\phi, n+1) = \phi \circ \operatorname{iter}(\phi, n)$
It's clear there's something wrong at the point that they have an equation with an x on one side but not the other. It should be $\operatorname{iter}(\phi, n)(x) = \phi^{n+1}(x)$
Similarly the definition of $\beta(0)$ is confusing at best. $\beta(0)(x) = x+1$ would be correct, or $\beta(0) = \lambda x.x + 1$
I'd try another source if I were you.