2
$\begingroup$

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?

$\endgroup$

2 Answers 2

7
$\begingroup$

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.

$\endgroup$
7
  • $\begingroup$ A mminor quibble: in the last sentence, it is better to say "by ordinal notations" or "by ordinal number notations". $\endgroup$ Jun 8, 2022 at 8:36
  • $\begingroup$ @AndrejBauer fair point. Edited. $\endgroup$ Jun 8, 2022 at 11:14
  • $\begingroup$ Really helpful answer, thanks! I have some reading to do $\endgroup$
    – Jonathan
    Jun 8, 2022 at 14:40
  • $\begingroup$ I think you're incorrect in invoking the Uzyczyn conjecture here Andras: typability of an (unannotated) term does not necessarily translate into the size of the computable functions $\mathbb{N}\rightarrow\mathbb{N}$: e.g. all normal forms are typeable in system F (but they aren't necessarily typed as functions $\mathbb{N}\rightarrow\mathbb{N}$) $\endgroup$
    – cody
    Jun 8, 2022 at 15:35
  • 1
    $\begingroup$ Kind of for the second one (but not for the first), let me write up an answer. $\endgroup$
    – cody
    Jun 8, 2022 at 19:45
6
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Did you mean "all of CoC can be accounted for"? $\endgroup$ Jun 8, 2022 at 21:38
  • $\begingroup$ No, but my phrasing is unclear: I meant "CSTT is a well-known theory that is also exactly at the same expressiveness". In some ways, CoC and CSTT are incomparable: CoC has dependent types, and CSTT has axioms. CSTT is an appropriate environment to formalize large parts of math, CoC needs at least a couple axioms to be suitable. $\endgroup$
    – cody
    Jun 8, 2022 at 21:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.