29
$\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

Improve this question
$\endgroup$
6
  • $\begingroup$ You may want to check this page but the list does not include the halting problem. $\endgroup$
    – Kaveh
    Commented Jan 14, 2011 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
    Commented Jan 14, 2011 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
    Commented Jan 14, 2011 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
    Commented Jan 14, 2011 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
    Commented Jan 14, 2011 at 11:37

1 Answer 1

Reset to default
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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.