*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Richard Waldinger <waldinger at AI.SRI.COM>*Date*: Wed, 30 Sep 2009 05:06:20 -0700*Cc*: isabelle-users at cl.cam.ac.uk, Wang Zirui <zirui at nus.edu.sg>*In-reply-to*: <4AC31798.7080205@in.tum.de>*References*: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com> <4AC31798.7080205@in.tum.de>

On Sep 30, 2009, at 1:32 AM, Alexander Krauss 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 HOLalso has a notion of a set, although it is not quite the same as inZFC.[...] 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 finiteautomata, 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

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

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

- Previous by Date: Re: [isabelle] Formalizing Turing machine
- Next by Date: Re: [isabelle] generate- pdf
- 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