Can you define functions which are not primitive recursive, yet total, in Type Theory? 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?
 A: $\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.
