Re: [isabelle] Formalizing Turing machine

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.


> 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

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