<p>Benjamin Werner has proved the mutual interpretability of ZFC with countably many inaccessibles and the Calculus of Inductive Constructions, in his paper <em><a href="http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709">Sets in Types, Types in Sets</a></em>.  </p>

<p>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. </p>

CC BY-SA 3.0
2012-01-17T20:10:16.590Z
Except a Coq interpreter...
Jules
CC BY-SA 3.0
2012-01-18T14:46:59.113Z
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
CC BY-SA 3.0
2012-01-18T19:11:43.863Z
How would you propose to implement it?
cody
CC BY-SA 3.0
2012-01-19T05:39:57.417Z
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
CC BY-SA 3.0
2012-01-19T07:22:45.627Z
@Neel: That's cheating. And for a good reason, otherwise we'd have an inconsistency.
Andrej Bauer
CC BY-SA 3.0
2012-01-19T07:23:53.037Z
So you are saying that ZFC with inaccessible cardinals does not prove termination of Coq normalization algorithm?
Andrej Bauer
CC BY-SA 3.0
2012-01-19T08:26:44.743Z
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
CC BY-SA 3.0
2012-01-20T16:40:05.833Z
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
CC BY-SA 3.0
2012-01-22T13:26:09.770Z
@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
CC BY-SA 3.0
2012-01-22T18:08:31.123Z
It is cheating because the evaluation function is supposed to *evaluate* things, not give you a non-answer.
Andrej Bauer
CC BY-SA 3.0
2012-01-17T11:49:05.273Z
2012-01-17T11:49:05.273Z
Neel Krishnaswami
<p>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?)</p>

<computability><pl.programming-languages><coq>
Class of functions computable by Coq
Steve
# Class of functions computable by Coq

(Asked by: username_0 on 2012-01-17)

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

**Tags:** computability, pl.programming-languages, coq

---

## 1 answers

### Answer by username_1 on 2012-01-17. Score: 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](http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709)*.

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.

> **Comments:**
> **username_2**: Except a Coq interpreter...  
> **username_1**: 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.  
> **username_3**: How would you propose to implement it?  
> **username_1**: 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.)  
> **username_4**: @Neel: That's cheating. And for a good reason, otherwise we'd have an inconsistency.  
> **username_4**: So you are saying that ZFC with inaccessible cardinals does not prove termination of Coq normalization algorithm?  
> **username_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.  
> **username_3**: 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...  
> **username_5**: @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.  
> **username_4**: It is cheating because the evaluation function is supposed to *evaluate* things, not give you a non-answer.  

---

