28
$\begingroup$

Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I downloaded and experimented with Coq, but it doesn't have a library for Turing machines. I thought to code one myself, but found the tutorial lacking and the language difficult to pick up.

My question is: Is there an automated theorem prover that is generally good at proving theorems that involve Turing machines? I would consider such a theorem prover "good" if it can formalize a proof of the undecidability of the halting problem using already-existing libraries. I would consider it even better if it's relatively easy to pick up. (For the record, I don't usually have difficulty with programming languages.)

Thanks,

Philip

$\endgroup$
  • $\begingroup$ You may want to check this page but the list does not include the halting problem. $\endgroup$ – Kaveh Jan 14 '11 at 5:21
  • 10
    $\begingroup$ I dare say that you need to persist with something like Coq before it will feel natural. And you need to be at the terminal working through problems, rather than reading the book. Getting your hands on "Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions" will help. Coq tutorials: cis.upenn.edu/~bcpierce/sf and adam.chlipala.net/cpdt are quite good (though not aimed directly at what you want). $\endgroup$ – Dave Clarke Jan 14 '11 at 8:08
  • 5
    $\begingroup$ Formalization of a proof can be quite complicated if you pick the "wrong" version of it. For the Halting problem I would suggest proving a more general and abstract version first. Then you can prove later that Turing machines are a special case of the abstract version, if you still feel like doing it (there will be very many tedious details about Turing machines so perhaps time would be better spent doing something else). I will think about a good way of proving this in Coq. Stayed tuned. $\endgroup$ – Andrej Bauer Jan 14 '11 at 8:16
  • 5
    $\begingroup$ If you are good at mathematics and good at programming, then you have the prerequisites to learn how to use a proof assistant. You really need to treat it as a new skill. (It is, however, very rewarding.) $\endgroup$ – Neel Krishnaswami Jan 14 '11 at 9:42
  • $\begingroup$ It looks like the answer to the question is "no". Such a system would be very useful I think - may I request that if you do formalize Turing machines, could you give a little thought to polynomial-time equivalence? $\endgroup$ – Colin McQuillan Jan 14 '11 at 11:37
17
$\begingroup$

Here is an Isabelle/HOL library containing Rice's theorem, which states undecidability of a wide range of problems. Since this library models computability via recursive functions, you have to encode a universal Turing machine as a recursive function in order to use this theorem for proving undecidability of the halting problem of Turing machines. However, the essential parts of the undecidability proof is already done.

http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.