*To*: zirui at nus.edu.sg*Subject*: Re: [isabelle] Formalizing Turing machine*From*: Konrad Slind <konrad.slind at gmail.com>*Date*: Thu, 1 Oct 2009 10:31:11 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <69C72A18-77BB-4FB2-89F4-378AD755A9E0@cs.utah.edu>*References*: <fb295f280910010234h2192737bieb34ed72bfaa451a@mail.gmail.com> <69C72A18-77BB-4FB2-89F4-378AD755A9E0@cs.utah.edu>

Hi Zirui, TMs can be represented by bitstrings (or numbers). No sets. A TM evaluator can be written that takes in a bitstring, decodes it into a TM and an input, and simulates the execution of the TM on the input. That evaluator can itself be written out as a bitstring representing a TM. Any decent undergrad theory textbook will go into this in some amount of detail. So there is a certain portion of computability theory that is basic programming and can be formalized in a simple logic that doesn't formalize set theory. On the other hand, much of computability is about infinite sets (not lists), some of which can be implemented by TMs and some which can't. Again, any undergrad theory text (or wikipedia) has plenty of detail. Cheers, Konrad. > > 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 > >

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

- Previous by Date: Re: [isabelle] Formalizing Turing machine
- Next by Date: [isabelle] file name of export_code
- 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