3

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

cody
  • 13,861
  • 1
  • 49
  • 103
Belleve Invis
  • 31
  • 1
  • 3
    Coq is Turing complete. The types simply have to make honest claims. – gallais Dec 04 '16 at 21:43
  • 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 Dec 05 '16 at 16:11
  • 1
    @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 Dec 05 '16 at 17:11
  • 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 Dec 05 '16 at 19:19
  • @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 Dec 08 '16 at 23:23
  • 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 Dec 09 '16 at 01:59

0 Answers0