Re: [isabelle] Formalizing Turing machine



didn't turing's original paper do a formalization? in some sort of number theory, i forget which logic.

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 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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.