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:
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
[...] 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