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?)
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
10
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.
answered Jan 17, 2012 at 11:49
-
7
-
6$\begingroup$ 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. $\endgroup$ Jan 18, 2012 at 14:46
-
2$\begingroup$ 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", dl.acm.org/citation.cfm?id=1616077.1616090.) $\endgroup$ Jan 19, 2012 at 5:39
-
1$\begingroup$ @Neel: That's cheating. And for a good reason, otherwise we'd have an inconsistency. $\endgroup$ Jan 19, 2012 at 7:22
-
2$\begingroup$ It is cheating because the evaluation function is supposed to evaluate things, not give you a non-answer. $\endgroup$ Jan 22, 2012 at 18:08