What is the computational power of the Calculus of Constructions?

Question

The calculus of constructions (CoC) without fix is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: Is there a decidable problem that cannot be computed in the CoC?

I found Statman's theorem, which says that the simply typed lambda calculus is limited computationally (I think? I find it hard to understand), but I'm pretty sure the CoC should be more powerful than the simply typed lambda calculus. Are there any theoretical results on that?

Answer 1

There is no total language where all total computable $\mathbb{N} \to \mathbb{N}$ functions are definable. In a total language, an interpreter for the same language is not definable because if it were then general recursion could be recovered by diagonalization; see theorem 3.2 here. This is analogous to Gödel's second incompleteness theorem.

The range of definable total functions in a theory is called proof-theoretic strength. The calculus of constructions has the same strength as System F$\omega$. That is in turn at least as strong as System F, and probably strictly stronger (see cody's answer). System F has the same strength as second-order arithmetic. You can read about this in chapter 15 of Girard's Proofs and Types. Second-order arithmetic is in turn weaker than ZFC, but it's strong enough to be beyond the reach of ordinal analysis, which tries to measure proof-theoretic strength by ordinal notations.

EDIT: taking cody's remarks into account.

Answer 2

My understanding of András' answer is that, while it gets the gist correct, his final conclusion is not quite right: The "standard" way to determine the strength of the function space in a logical calculus, like CoC is traditionally via realizability, as was used by Girard to justify the strength of $\mathrm{HA}_2$ having exactly the nat -> nat functions of system F as definable functions.

However in CoC, it's possible to directly look at the proof terms, and "erase" parts of it to obtain system $\mathrm{F}_\omega$ terms, which have the same reduction behavior in the case of nat -> nat functions. This is done in detail in section 5.3 of Barendregt's Lambda Calculi with Types, which he attributes to Berardi.

I suspect a realizability argument along the lines of the one given by Berger and Hou in A realizability interpretation of Church's simple theory of types would additionally show that all of Church's simple type theory can be accounted for, i.e. the provably definable functions of that theory are exactly those definable in system $\mathrm{F}_\omega$.

This would mean that there are strictly more such functions in CoC than in system F, by some standard Gödelian argument.

Why does this not contradict the conjecture András refers to? I actually asked this to Pawel Uzyczyn a while back: the question asked there is actually about which untyped terms can be assigned some type in various systems. There is no guarantee that $\mathrm{F}_\omega$ and $\mathrm{F}_1$ would assign the same type, much less the type nat -> nat! As such, the question is more about type assignment systems than logical theories.