Generalized Recursion vs. Turing Completeness

ackermann-functionrecursiontype-theory

$\newcommand{\NN}{\mathbb N}\newcommand{\UU}{\mathcal U}$I'm currently reading through Homotopy Type Theory: Univalent Foundations of Mathematics. In Exercise 1.10, we construct the Ackermann function using (their version of) primitive recursion, which surprised me because I'm used to having the Ackermann function being a function between primitive recursion and computability.

Of course, what makes the exercise possible is that we can recurse over not just $\NN$ but over functions $\NN\to\NN.$ Roughly speaking, the fact we can define $\textsf{ack}(m+1)$ in terms of $\textsf{ack}(m)$ is enough to recursively define the Ackermann function $\textsf{ack}:\NN\to\NN\to\NN.$

Anyways, being able to recurse over arbitrary types seems like a lot of power, and I was wondering exactly how much power.

Is there a total computable function $\NN\to\NN$ which cannot be formed from the above "generalized" primitive recursion?

I suspect one to exist. If there's a finer line between what generalized primitive recursion gives and computable enumerability, I'd be interested in that too.

Best Answer

The range of total computable $\mathbb{N} \to \mathbb{N}$ functions definable in a type theory corresponds to the proof-theoretic strength of the theory.

There is no total language for all total computable $\mathbb{N} \to \mathbb{N}$ functions. This is a constructive analogue to Gödel's second incompleteness theorem. If such a language existed, it would also contain its self-interpreter function for a suitable $\mathbb{N}$-encoding of programs, but that would make it possible to write general recursive programs, contradicting totality.

For some type theories, the range of definable functions can be concisely characterized by an ordinal number. In this case, we have an ordinal number $\alpha$ such that the fast-growing function $f_{\alpha} : \mathbb{N} \to \mathbb{N}$ grows faster than any definable function in the theory. Here's a listing of ordinals for some type theories.

For any type theory with an impredicative universe, no proof-theoretic ordinal is known. Here the strength of the theory can be explained by comparison to other systems. As Dan Doel mentioned, System F (a non-dependent stratified theory with an impredicative universe) has the same strength as second-order arithmetic.

Simple type theory with $\mathbb{N}$ is also known as Gödel's System T, and has strength $\epsilon_0$. This is stronger than primitive recursive arithmetic; the Ackermann function is definable in System T but not in PRA. The System-T-definable functions are also precisely the functions which are provably total in Peano Arithmetic. Calling the recursion principle of System T (or HoTT) "primitive recursion" is a bit confusing, because it's not the same thing as the recursion principle in PRA.

Infinitary inductive types (such as W-types) increase strength in predicative theories significantly. Intuitively, that's because their induction principles immediately provide a form of transfinite induction.

Is there a total computable function ℕ→ℕ which cannot be formed from the above "generalized" primitive recursion?

It depends on what other features are supported in the type theory. If we only have $\mathbb{N}$ and functions, $f_{\epsilon_0}$, Goodstein sequences and hydra games are examples for undefinable functions. If we have infinitary inductive types (or W-types), we get a power boost and we can easily define these functions. For example, in Agda we can define $f_{\epsilon_0}$ in the following way:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data O : Set where
  zero : O
  suc  : O → O
  lim  : (ℕ → O) → O     -- ℕ-branching node (infinitary)

iter : {A : Set} → ℕ → (A → A) → A → A
iter zero    f a = a
iter (suc n) f a = f (iter n f a)

f : O → ℕ → ℕ
f zero    n = n
f (suc α) n = iter n (f α) n
f (lim g) n = f (g n) n

_+_ : O → O → O
α + zero  = α
α + suc β = suc (α + β)
α + lim f = lim (λ n → α + f n)

_*_ : O → O → O
α * zero  = zero
α * suc β = (α * β) + α
α * lim f = lim (λ n → α * f n)

_^_ : O → O → O
α ^ zero  = suc zero
α ^ suc β = (α ^ β) * α
α ^ lim f = lim (λ n → α ^ f n)

ω : O
ω = lim (λ n → iter n suc zero)

fε₀ : ℕ → ℕ
fε₀ = f (lim (λ n → iter n (ω ^_) ω))
Related Question