25

Since it does not allow nonterminating computation, Coq is necessarily not Turing-complete. What is the class of functions that Coq can compute? (is there an interesting characterization thereof?)

Sam Tobin-Hochstadt
  • 1,897
  • 11
  • 21
Steve
  • 251
  • 2
  • 3

1 Answers1

21

Benjamin Werner has proved the mutual interpretability of ZFC with countably many inaccessibles and the Calculus of Inductive Constructions, in his paper Sets in Types, Types in Sets.

This means, roughly, that any function which can be shown to be total in ZFC with countably many inaccessibles can be defined in Coq. So unless you are a set theorist working on large cardinals, it is unlikely that any computable function you have ever wanted cannot be defined in Coq.

Neel Krishnaswami
  • 32,528
  • 1
  • 100
  • 165
  • 7
    Except a Coq interpreter... – Jules Jan 17 '12 at 20:10
  • 6
    Actually, you can implement a Coq interpreter (indeed, arbitrary general recursive functions) inside Coq. If CIC is consistent, you won't be able to prove that the interpreter is a total function, of course, but you can definitely implement it. – Neel Krishnaswami Jan 18 '12 at 14:46
  • How would you propose to implement it? – cody Jan 18 '12 at 19:11
  • 2
    You can use the constructive lift monad, $A_\bot \triangleq \nu \alpha.; A + \alpha$, to write general recursive functions. Then your typechecker will have type $\mathsf{context} \to \mathsf{term} \to \mathsf{type} \to \mathsf{bool}_\bot$. This is basically the Bove/Capretta approach. (See also Benton, Kennedy and Varming's "Some Domain Theory and Denotational Semantics in Coq", http://dl.acm.org/citation.cfm?id=1616077.1616090.) – Neel Krishnaswami Jan 19 '12 at 05:39
  • 1
    @Neel: That's cheating. And for a good reason, otherwise we'd have an inconsistency. – Andrej Bauer Jan 19 '12 at 07:22
  • So you are saying that ZFC with inaccessible cardinals does not prove termination of Coq normalization algorithm? – Andrej Bauer Jan 19 '12 at 07:23
  • 1
    As I understand it, there are extensions of Werner's proof-irrelevant semantics which do show normalization of CIC. Since this semantics uses inaccessibles at every level, the semantic interpretation itself will not be an object of ZFC with inaccessibles. – Neel Krishnaswami Jan 19 '12 at 08:26
  • You just need big enough inaccessibles :) And as usual I believe Andrej is right, I don't think it is possible to have a term of type context -> term -> type -> bool that computes whether a term type-checks: such a term exists if and only if the function is provably definable in the logic... – cody Jan 20 '12 at 16:40
  • 1
    @AndrejBauer: I disagree that this is "cheating". You can write a total one-step reduction function for CIC, and then let the user do the coinductive work of chaining reductions and deciding how far he want to go (eg. by providing an integer argument as "fuel"); or pose termination as an axiom, to get the normalization function. The point is that you did the useful/interesting work in a safe way inside the framework, and you isolated precisely the non-provable part. Similarly, it would be interesting to see how far you can go in a termination proof, admittng only a simple strength principle. – gasche Jan 22 '12 at 13:26
  • 2
    It is cheating because the evaluation function is supposed to evaluate things, not give you a non-answer. – Andrej Bauer Jan 22 '12 at 18:08