Can you define functions which are not primitive recursive, yet total, in Type Theory? [closed]

Solution 1:

$\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 = a\ m\ 1 \\ &\ack\ (\suc m)\ (\suc n) = a\ m\ (a\ (\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.