Re: [isabelle] Formalizing Turing machine

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:

It's not Turing Machines, but it may give you an idea...


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