# Class of functions computable by Coq

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?)

## 1 Answer

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.

• Except a Coq interpreter... – Jules Jan 17 '12 at 20:10
• 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
• 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.) – Neel Krishnaswami Jan 19 '12 at 5:39
• @Neel: That's cheating. And for a good reason, otherwise we'd have an inconsistency. – Andrej Bauer Jan 19 '12 at 7:22
• 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