*To*: Konrad Slind <slind at cs.utah.edu>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Wang Zirui <zirui at nus.edu.sg>*Date*: Thu, 1 Oct 2009 17:34:59 +0800*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <484D4747-C069-4492-8966-30C759670E56@cs.utah.edu>*References*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com> <484D4747-C069-4492-8966-30C759670E56@cs.utah.edu>

I'm sorry, but I'd like to repeat again that I'm not talking about programming tricks. So lists are as high level as sets, because you can implement sets by lists. Actually I don't mean sets in particular but rather *set theory*. I want to avoid the use of sets because I want to have nothing to do with the axioms of set theory. So lists probably also rely on the axioms of set theory, unless you can define it without the axioms of set theory. So let repeat my question: Can we define Turing machine without relying on the axioms of set theory? I think part of the misconception is because I'm posting this topic under Isabelle. Actually my question has nothing to do with Isabelle or HOL; I just imagined that people here might be good at formalizing concepts and proofs using rudimentary logic theory. Sorry for the misunderstanding. Zirui On Wed, Sep 30, 2009 at 10:49 PM, Konrad Slind <slind at cs.utah.edu> wrote: > 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. > > > (*---------------------------------------------------------------------------*) > (* Turing machines, tape infinite in one direction. > *) > (*---------------------------------------------------------------------------*) > > Hol_datatype `dir = L | R`; > > (*---------------------------------------------------------------------------*) > (* Raw datatype of TMs. The only slightly odd thing may be that the blank is > *) > (* explicitly included. Also, it turns out to facilitate the definition of > *) > (* executions if the initial value of the current cell is set to a value. > *) > (* Because having a "left-edge" marker simplifies many TM algorithms, we set > *) > (* aside a particular "star" value for this purpose. > *) > (*---------------------------------------------------------------------------*) > > 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 |>`; > (*---------------------------------------------------------------------------*) > (* Predicate singling out the real Turing machines. Is in principle an > *) > (* executable thing, but we don't currently handle (bounded) quantifiers. > *) > (*---------------------------------------------------------------------------*) > > 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.

**Follow-Ups**:**Re: [isabelle] Formalizing Turing machine***From:*Lawrence Paulson

**Re: [isabelle] Formalizing Turing machine***From:*Tjark Weber

- Previous by Date: Re: [isabelle] Formalizing Turing machine
- Next by Date: Re: [isabelle] Formalizing Turing machine
- Previous by Thread: Re: [isabelle] Formalizing Turing machine
- Next by Thread: Re: [isabelle] Formalizing Turing machine
- Cl-isabelle-users October 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