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 '16 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 '16 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 '16 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 '16 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 '16 at 23:23