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

  • 3
    $\begingroup$ Coq is Turing complete. The types simply have to make honest claims. $\endgroup$
    – gallais
    Dec 4, 2016 at 21:43
  • $\begingroup$ 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: cstheory.stackexchange.com/questions/24986/… $\endgroup$
    – cody
    Dec 5, 2016 at 16:11
  • 1
    $\begingroup$ @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). $\endgroup$
    – chi
    Dec 5, 2016 at 17:11
  • $\begingroup$ 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. $\endgroup$
    – gallais
    Dec 5, 2016 at 19:19
  • $\begingroup$ @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. $\endgroup$
    – Kaveh
    Dec 8, 2016 at 23:23


Browse other questions tagged or ask your own question.