*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Wang Zirui <zirui at nus.edu.sg>*Date*: Wed, 30 Sep 2009 17:25:29 +0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4AC31798.7080205@in.tum.de>*References*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com> <4AC31798.7080205@in.tum.de>

Hi Alex, The point of not relying on ZFC is because it's a strong theory. I don't want the definition of Turing machine to be based on a strong theory. I want it to be based on a theory that is as weak as possible. So it's best if it's based on nothing. Unfortunately HOL is at least as strong as ZFC because it has the idea of a set. My teacher Jain suggests that it might be possible to define Turing machine based on Peano Arithmetic, which is weaker than ZFC. And I'm going to try that. I don't understand the AFP formalization of automata as I read it. Does the author use the idea of sets, functions or numbers? If yes, he probably base the definition of automata on HOL or ZFC. But I want to base it on a weaker theory. Does the author do that? Your suggestion of automata is certainly good as it has the same problem as Turing machines, but it's simpler. Regards, Zirui On Wed, Sep 30, 2009 at 4:32 PM, Alexander Krauss <krauss at in.tum.de> wrote: > Deac Zirui, > >> 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. > > There should be no problems with doing it in HOL. Note that HOL also has a > notion of a set, although it is not quite the same as in ZFC. > >> [...] So if you agree with me and think it's possible to go >> without sets, could you please outline how to define Turing machine? > > You may want to look at Tobias Nipkow's formalization of finite automata, > which you can find in the AFP: > > http://afp.sourceforge.net/entries/Functional-Automata.shtml > > It's not Turing Machines, but it may give you an idea... > > Alex >

**Follow-Ups**:**Re: [isabelle] Formalizing Turing machine***From:*Alexander Krauss

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

**Re: [isabelle] Formalizing Turing machine***From:*Alexander Krauss

- Previous by Date: [isabelle] Polymorphic parameter in locales
- 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 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