Re: [isabelle] Formalizing Turing machine


  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


(*---------------------------------------------------------------------- -----*) (* 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. *) (*---------------------------------------------------------------------- -----*)

  `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 =
   `isTM (M : ('alpha,'state)TM) =
      FINITE M.states            /\
      FINITE M.inputsymbs        /\
      FINITE M.tapesymbs         /\
      M.blank IN M.tapesymbs     /\
      ~(M.blank IN M.inputsymbs) /\ 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`;


On Sep 29, 2009, at 3:39 AM, Wang Zirui 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.

Yes, in the definition of Turing machine we see sets, such as the set
of states, but I think the use of set is convenient but not necessary.
(Am I wrong?) So if you agree with me and think it's possible to go
without sets, could you please outline how to define Turing machine?
If you think this is impossible, can you give a proof?


Zirui Wang

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