*To*: Wang Zirui <zirui at nus.edu.sg>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Konrad Slind <slind at cs.utah.edu>*Date*: Wed, 30 Sep 2009 08:49:58 -0600*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com>*References*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com>

Hi, Yes, you can define Turing machines in a very simple base theory. For example, you can use lists instead of sets because everything in a TM description has to be finite. So at least the preliminary theory of TMs can be done without higher order things like sets and functions. But going even a little bit into the theory, you will need to define computable functions etc. On the face of it, even the undecidability of the Halting Problem seems to need sets to state (i.e. the *set* of all halting TMs is undecidable). I did some work on formalizing TMs in HOL-4 and the following definitions of the machines should be completely straightforward to turn into Isabelle/HOL syntax. Of course there is more to define, like machine configurations, executions, languages, etc. but I will omit those. Also, doesn't the AFP include some computability theory already? Cheers, Konrad.

Hol_datatype `dir = L | R`;

Hol_datatype `TM = <| states : 'state -> bool ; inputsymbs : 'alpha -> bool ; tapesymbs : 'alpha -> bool ; init : 'state ; trans : 'state -> 'alpha -> 'state # 'alpha # dir; accept : 'state ; reject : 'state ; blank : 'alpha ; star : 'alpha |>`;

val isTM_def = Define `isTM (M : ('alpha,'state)TM) = FINITE M.states /\ FINITE M.inputsymbs /\ FINITE M.tapesymbs /\ M.blank IN M.tapesymbs /\ ~(M.blank IN M.inputsymbs) /\ M.star IN M.inputsymbs /\ M.inputsymbs SUBSET M.tapesymbs /\ M.accept IN M.states /\ M.reject IN M.states /\ ~(M.accept = M.reject) /\ M.init IN M.states /\ !a p q b d. a IN M.tapesymbs /\ p IN M.states /\ (M.trans p a = (q,b,d)) ==> q IN M.states /\ b IN M.tapesymbs`; Cheers, Konrad. On Sep 29, 2009, at 3:39 AM, Wang Zirui wrote:

Hi, I'd like to formalize the definition of Turing machine. If possible, I'd like to do it without relying on ZFC. That is, I don't use sets, integers and so on. Yes, in the definition of Turing machine we see sets, such as the set of states, but I think the use of set is convenient but not necessary. (Am I wrong?) So if you agree with me and think it's possible to go without sets, could you please outline how to define Turing machine? If you think this is impossible, can you give a proof? Thanks. Regards, Zirui Wang

**References**:**[isabelle] Formalizing Turing machine***From:*Wang Zirui

- Previous by Date: Re: [isabelle] generate- pdf
- Previous by Thread: Re: [isabelle] Formalizing Turing machine
- Next by Thread: [isabelle] Polymorphic parameter in locales
- Cl-isabelle-users September 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list