Ackermann's function is total but not primitive recursive. Can one define Ackermann's function in Type Theory,
ie:
Can you define functions which are not primitive recursive, yet total, in Type Theory?
[this post was closed] due to being "not specific enough", however this question is very specific, to the point. It is exactly what I need to know, and no more can be asked. What exactly is meant by being more specific here?
$\newcommand{\suc}{\mathsf{suc}\ }$ $\newcommand{\iter}{\mathsf{iter}}$ $\newcommand{\ack}{\mathsf{ack}}$ The Ackermann function can be defined in e.g. Martin-löf type theory. The reason is that the notion of 'primitive recursion' that you are able to use is much stronger due to the presence of higher-order functions. Here is how you might go about figuring out how.
The specification is:
$$ \begin{align} &\ack\ 0\ n = n + 1 \\ &\ack\ (\suc m)\ 0 = \ack\ m\ 1 \\ &\ack\ (\suc m)\ (\suc n) = \ack\ m\ (\ack\ (\suc m)\ n) \end{align} $$
The thing to notice is that $\ack\ (\suc m)\ n$ is the (n+1)-fold composition of $\ack\ m$ applied to $1$, and $\ack\ 0$ is $\mathsf{suc}$. So, if we define:
$$ \begin{align} &\iter : ℕ → (A → A) → A → A \\ &\iter\ 0\ f = f \\ &\iter\ (\suc n)\ f = f \circ \iter\ n\ f \end{align} $$
which is a recursive definition of the (n+1)-fold composition. Then we can define:
$$ \begin{align} &\ack : ℕ → (ℕ → ℕ) \\ &\ack\ 0 = \suc \\ &\ack\ (\suc m) = λ n → \iter\ n\ (\ack\ m)\ 1 \end{align} $$
which is also acceptable recursion on $ℕ$.
These definitions aren't allowed under the traditional rules of primitive recursion, because a primitive recursive definition must be of a first-order function, with type like $ℕ × ... × ℕ → ℕ$. But, a theory that lets you define higher-order functions 'by primitive recursion' will let you go beyond this.