4 ms·
I am not aware of his definition? I can't find it on google either. Can you point me to it? A Turing machine does not talk about expressing computations, but r
by madsbuch 9y ago
I am not aware of his definition? I can't find it on google either. Can you point me to it?
A Turing machine does not talk about expressing computations, but rather a class of problems that can be computed.
Remember, not all programming languages are Turing complete (Coq being one of them).
- gerdesj 9y agoI can still hear "whoosh" in my own ears here 8) Given how simple a Turing Machine can be, I seriously doubt (without any proof) that coq is not able to recreate a TM. I am not an expert but the explanation about Turing Machines I read was in GED and involved a simple tape and a slack handful of symbols and operations and some basic hand waving. If coq can't manage that then it is unlikely to be useful - which I doubt.
- madsbuch 9y agoYou should check you ears. Coq only accepts well funded recursion. Non-bound Turing machines span a bigger complexity class. In other words: Turing machines can loop forever, Coq can not express programs that can do so. Read your CS 101: