<p>Given that all functions in Coq will terminate, it cannot cover the entire $RE$. So what is the class it can achieve? Is it $R$?</p>

CC BY-SA 3.0
2016-12-04T21:43:20.887Z
[Coq is Turing complete](https://gist.github.com/gallais/28e01f92bd93144e8e1e5771943fbedf). The types simply have to make honest claims.
gallais
CC BY-SA 3.0
2016-12-05T16:11:30.957Z
It's probably useful to note that it *cannot* be $R$: a language like Coq with only terminating functions will fall prey to a diagonalization argument like in the top answer to this question: http://cstheory.stackexchange.com/questions/24986/a-total-language-that-only-a-turing-complete-language-can-interpret?rq=1
cody
CC BY-SA 3.0
2016-12-05T17:11:34.040Z
@gallais I'm not entirely sure if I would call Coq Turing complete because of that. I mean, even using only primitive recursion you can write a function which simulates a TM for $k$ steps ($k$ being a parameter). This is not too different from that Coinductive type, I think(?). Coq has higher order primitive recursion, though, which makes it far more powerful than PR (e.g. it can define the Ackermann function).
chi
CC BY-SA 3.0
2016-12-05T19:19:16.283Z
The difference is that using `Delay`, it is truly possible to express *the whole computation* and not just all of its prefixes of finite length.
gallais
CC BY-SA 3.0
2016-12-08T23:23:36.803Z
@gallais, Turing-complete has a specific meaning. You can encode and decode computation rather easily in general (take e.g. $AC^0_4$), and a theory as week as $V^0$ can do it. The reason class of functions or a theory ends up being smaller than computable function is typically a consequence of lack of functions that grow fast enough. I would suggest checking out the book "Classical Recursion Theory" if you are interested in the topic. You should be able to prove those functions are total and to do that you need a function that upper bounds the size of computation.
Kaveh
CC BY-SA 3.0
2016-12-09T01:59:41.387Z
The title question is not addressed nor answered in the proposed duplicate. The body of the question is easily answerable in the negative.
François G. Dorais
<computability><coq><proof-theory>
What is the largest complexity class that a non-Turing complete proof assitant, like Coq, can achieve?
Belleve Invis
# What is the largest complexity class that a non-Turing complete proof assitant, like Coq, can achieve?

(Asked by: username_0 on 2016-12-04)

Given that all functions in Coq will terminate, it cannot cover the entire $RE$. So what is the class it can ausername_3eve? Is it $R$?

**Tags:** computability, coq, proof-theory

> **Comments:**
> **username_1**: [Coq is Turing complete](https://gist.github.com/username_1/28e01f92bd93144e8e1e5771943fbedf). The types simply have to make honest claims.  
> **username_2**: It's probably useful to note that it *cannot* be $R$: a language like Coq with only terminating functions will fall prey to a diagonalization argument like in the top answer to this question: http://cstheory.stackexchange.com/questions/24986/a-total-language-that-only-a-turing-complete-language-can-interpret?rq=1  
> **username_3**: @username_1 I'm not entirely sure if I would call Coq Turing complete because of that. I mean, even using only primitive recursion you can write a function which simulates a TM for $k$ steps ($k$ being a parameter). This is not too different from that Coinductive type, I think(?). Coq has higher order primitive recursion, though, which makes it far more powerful than PR (e.g. it can define the Ackermann function).  
> **username_1**: The difference is that using `Delay`, it is truly possible to express *the whole computation* and not just all of its prefixes of finite length.  
> **username_4**: @username_1, Turing-complete has a specific meaning. You can encode and decode computation rather easily in general (take e.g. $AC^0_4$), and a theory as week as $V^0$ can do it. The reason class of functions or a theory ends up being smaller than computable function is typically a consequence of lack of functions that grow fast enough. I would suggest checking out the book "Classical Recursion Theory" if you are interested in the topic. You should be able to prove those functions are total and to do that you need a function that upper bounds the size of computation.  
> **username_5**: The title question is not addressed nor answered in the proposed duplicate. The body of the question is easily answerable in the negative.  

---

## 0 answers

