I'm reading through https://plato.stanford.edu/entries/recursive-functions/ and came across a confusing part:
One means of doing so is to first use recursion on the type ℕ→ℕ—a simple form of recursion at higher types as envisioned by Skolem and Hilbert—to define an iteration functional as follows: $$Iter(,0) = $$ $$Iter(, x+1) = (Iter(, x))$$ $Iter$ takes as arguments a function $:ℕ→ℕ$ as well as a number $x∈ℕ$ and is defined so that $Iter(,n)=^{n+1}(x)$—i.e., the function which is the $n$th iterate of $$
Following from the base case, $Iter$ should return a function of type $ℕ→ℕ$. In the inductive clause, though, the output of $Iter$ is used as an argument to $$. But $$ expects a natural number, not another function. What am I missing here?
EDIT
As noted in the comments the formula should be $Iter(\phi, x+1)=\phi \circ Iter(\phi, x)$. But right after that $\beta$ function is introduced:
$$\beta(0)=x+1 (i.e., the successor function)$$ $$\beta(x+1)=Iter(\beta,x)$$
From the base case, $\beta$ is $ℕ→(ℕ→ℕ)$. But in the inductive clause, it's used as an argument for $Iter$, which is supposed to take only functions of type $ℕ→ℕ$. Should it be $\beta(x+1)=Iter(\beta(x),x)$ or something alike or the definition of $Iter$ should be changes once again?