# Re: [isabelle] Formalizing Turing machine

• To: Konrad Slind <slind at cs.utah.edu>
• Subject: Re: [isabelle] Formalizing Turing machine
• From: Wang Zirui <zirui at nus.edu.sg>
• Date: Thu, 1 Oct 2009 17:34:59 +0800
• Cc: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
• References: <fb295f280909290239k28b8ce6fm1693af3d26781795@mail.gmail.com> <484D4747-C069-4492-8966-30C759670E56@cs.utah.edu>

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

On Wed, Sep 30, 2009 at 10:49 PM, Konrad Slind <slind at cs.utah.edu> wrote:
> Hi,
>
>  Yes, you can define Turing machines in a very
> simple base theory. For example, you can use lists
> instead of sets because everything in a TM description
> has to be finite. So at least the preliminary theory
> of TMs can be done without higher order things like
> sets and functions. But going even a little bit into the
> theory, you will need to define computable functions etc.
> On the face of it, even the undecidability of the Halting
> Problem seems to need sets to state (i.e. the *set* of all
> halting TMs is undecidable).
>
>  I did some work on formalizing TMs in HOL-4 and the
> following definitions of the machines should be
> completely straightforward to turn into Isabelle/HOL syntax.
> Of course there is more to define, like machine configurations,
> executions, languages, etc. but I will omit those.
>
> Also, doesn't the AFP include some computability theory
>
> Cheers,
>
>
> (*---------------------------------------------------------------------------*)
> (* Turing machines, tape infinite in one direction.
>  *)
> (*---------------------------------------------------------------------------*)
>
> Hol_datatype `dir = L | R`;
>
> (*---------------------------------------------------------------------------*)
> (* Raw datatype of TMs. The only slightly odd thing may be that the blank is
> *)
> (* explicitly included. Also, it turns out to facilitate the definition of
> *)
> (* executions if the initial value of the current cell is set to a value.
>  *)
> (* Because having a "left-edge" marker simplifies many TM algorithms, we set
> *)
> (* aside a particular "star" value for this purpose.
> *)
> (*---------------------------------------------------------------------------*)
>
> Hol_datatype
>  `TM = <| states     : 'state -> bool ;
>           inputsymbs : 'alpha -> bool ;
>           tapesymbs  : 'alpha -> bool ;
>           init       : 'state ;
>           trans      : 'state -> 'alpha -> 'state # 'alpha # dir;
>           accept     : 'state ;
>           reject     : 'state ;
>           blank      : 'alpha ;
>           star       : 'alpha |>`;
> (*---------------------------------------------------------------------------*)
> (* Predicate singling out the real Turing machines. Is in principle an
> *)
> (* executable thing, but we don't currently handle (bounded) quantifiers.
>  *)
> (*---------------------------------------------------------------------------*)
>
> val isTM_def =
>  Define
>   `isTM (M : ('alpha,'state)TM) =
>      FINITE M.states            /\
>      FINITE M.inputsymbs        /\
>      FINITE M.tapesymbs         /\
>      M.blank IN M.tapesymbs     /\
>      ~(M.blank IN M.inputsymbs) /\
>      M.star IN M.inputsymbs     /\
>      M.inputsymbs SUBSET M.tapesymbs /\
>      M.accept IN M.states       /\
>      M.reject IN M.states       /\
>      ~(M.accept = M.reject)     /\
>      M.init IN M.states         /\
>      !a p q b d.
>          a IN M.tapesymbs /\ p IN M.states /\ (M.trans p a = (q,b,d))
>          ==> q IN M.states /\ b IN M.tapesymbs`;
>
>
> Cheers,