(*<*)

theory Paper

imports "../thys/uncomputable"

begin

(*

hide_const (open) s 

*)

abbreviation

  "update2 p a \<equiv> update a p"

consts DUMMY::'a

notation (latex output)

  Cons ("_::_" [78,77] 73) and

  set ("") and

  W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and

  W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and

  update2 ("update") and

(*  abc_lm_v ("lookup") and

  abc_lm_s ("set") and*)

  haltP ("stdhalt") and 

  tcopy ("copy") and 

  tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 

  tm_comp ("_ \<oplus> _") and 

  DUMMY  ("\<^raw:\mbox{$\_$}>")

declare [[show_question_marks = false]]

(*>*)

section {* Introduction *}

text {*

\noindent

whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work

where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}

is always provable no matter whether @{text P} is constructed by

\begin{quote}

\it``If register machines are unappealing because of their 

daunting prospect.''

\end{quote}

\noindent

In this paper we take on this daunting prospect and provide a

formalisation of Turing machines, as well as abacus machines (a kind

of register machines) and recursive functions. To see the difficulties

\cite{AspertiRicciotti12}. They describe a complete formalisation of

Turing machines in the Matita theorem prover, including a universal

Turing machine. They report that the informal proofs from which they

started are \emph{not} ``sufficiently accurate to be directly usable as a

guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For

our formalisation we followed mainly the proofs from the textbook

\cite{Boolos87} and found that the description there is quite

detailed. Some details are left out however: for example, it is only

shown how the universal Turing machine is constructed for Turing

machines computing unary functions. We had to figure out a way to

generalise this result to $n$-ary functions. Similarly, when compiling

recursive functions to abacus machines, the textbook again only shows

how it can be done for 2- and 3-ary functions, but in the

formalisation we need arbitrary functions. But the general ideas for

The main difference between our formalisation and the one by Asperti

and Ricciotti is that their universal Turing machine uses a different

alphabet than the machines it simulates. They write \cite[Page

23]{AspertiRicciotti12}:

\begin{quote}\it

``In particular, the fact that the universal machine operates with a

different alphabet with respect to the machines it simulates is

annoying.'' 

\end{quote}

\noindent

In this paper we follow the approach by Boolos et al \cite{Boolos87},

which goes back to Post \cite{Post36}, where all Turing machines

operate on tapes that contain only \emph{blank} or \emph{occupied} cells

(represented by @{term Bk} and @{term Oc}, respectively, in our

formalisation). Traditionally the content of a cell can be any

character from a finite alphabet. Although computationally equivalent,

the more restrictive notion of Turing machines in \cite{Boolos87} makes

the reasoning more uniform. In addition some proofs \emph{about} Turing

machines are simpler.  The reason is that one often needs to encode

Turing machines---consequently if the Turing machines are simpler, then the coding

functions are simpler too. Unfortunately, the restrictiveness also makes

it harder to design programs for these Turing machines. In order

to construct a universal Turing machine we therefore do not follow 

\cite{AspertiRicciotti12}, instead follow the proof in

\cite{Boolos87} by relating abacus machines to Turing machines and in

turn recursive functions to abacus machines. The universal Turing

machine can then be constructed as a recursive function.

\smallskip

\noindent

{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the

description of Boolos et al \cite{Boolos87} where tapes only have blank or

occupied cells. We mechanise the undecidability of the halting problem and

prove the correctness of concrete Turing machines that are needed

in this proof; such correctness proofs are left out in the informal literature.  

We construct the universal Turing machine from \cite{Boolos87} by

relating recursive functions to abacus machines and abacus machines to

Turing machines. Since we have set up in Isabelle/HOL a very general computability

model and undecidability result, we are able to formalise the

undecidability of Wang's tiling problem. We are not aware of any other

formalisation of a substantial undecidability problem.

*}

section {* Turing Machines *}

text {* \noindent

  Turing machines can be thought of as having a read-write-unit, also

  referred to as \emph{head},

  ``gliding'' over a potentially infinite tape. Boolos et

  al~\cite{Boolos87} only consider tapes with cells being either blank

  or occupied, which we represent by a datatype having two

  constructors, namely @{text Bk} and @{text Oc}.  One way to

  represent such tapes is to use a pair of lists, written @{term "(l,

  r)"}, where @{term l} stands for the tape on the left-hand side of the

  head and @{term r} for the tape on the right-hand side. We have the

  convention that the head, abbreviated @{term hd}, of the right-list is

  the cell on which the head of the Turing machine currently operates. This can

  be pictured as follows:

  \begin{center}

  \begin{tikzpicture}

  \draw[very thick] (-3.0,0)   -- ( 3.0,0);

  \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);

  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);

  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

  \draw[very thick] (-1.75,0)   -- (-1.75,0.5);

  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

  \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);

  \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);

  \draw[fill]     (-0.35,0.1) rectangle (-0.65,0.4);

  \draw (-0.25,0.8) -- (-0.25,-0.8);

  \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);

  \node [anchor=base] at (-0.8,-0.5) {\small left list};

  \node [anchor=base] at (0.35,-0.5) {\small right list};

  \node [anchor=base] at (0.1,0.7) {\small head};

  \node [anchor=base] at (-2.2,0.2) {\ldots};

  \node [anchor=base] at ( 2.3,0.2) {\ldots};

  \end{tikzpicture}

  \end{center}

  \noindent

  Note that by using lists each side of the tape is only finite. The

  potential infinity is achieved by adding an appropriate blank or occupied cell 

  whenever the head goes over the ``edge'' of the tape. To 

  make this formal we define five possible \emph{actions} 

  the Turing machine can perform:

  \begin{center}

  @{text "a"} & $::=$  & @{term "W0"} & write blank (@{term Bk})\\

  & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\

  & $\mid$ & @{term L} & move left\\

  & $\mid$ & @{term R} & move right\\

  & $\mid$ & @{term Nop} & do-nothing operation\\

  \end{tabular}

  \end{center}

  \noindent

  We slightly deviate

  from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use

  will become important when we formalise halting computations and also universal Turing 

  machines. Given a tape and an action, we can define the

  following tape updating function:

  \begin{center}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  @{thm (lhs) update.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(1)}\\

  @{thm (lhs) update.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(2)}\\

  @{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(5)}\\

  \end{tabular}

  \end{center}

  \noindent

  The first two clauses replace the head of the right-list

  with a new @{term Bk} or @{term Oc}, respectively. To see that

  these two clauses make sense in case where @{text r} is the empty

  list, one has to know that the tail function, @{term tl}, is defined in

  Isabelle/HOL

  such that @{term "tl [] == []"} holds. The third clause 

  implements the move of the head one step to the left: we need

  to test if the left-list @{term l} is empty; if yes, then we just prepend a 

  blank cell to the right-list; otherwise we have to remove the

  head from the left-list and prepend it to the right-list. Similarly

  in the fourth clause for a right move action. The @{term Nop} operation

  leaves the the tape unchanged (last clause).

  Next we need to define the \emph{states} of a Turing machine.  Given

  how little is usually said about how to represent them in informal

  presentations, it might be surprising that in a theorem prover we

  have to select carefully a representation. If we use the naive

  representation where a Turing machine consists of a finite set of

  states, then we will have difficulties composing two Turing

  machines: we would need to combine two finite sets of states,

  possibly renaming states apart whenever both machines share

  states.\footnote{The usual disjoint union operation in Isabelle/HOL

  cannot be used as it does not preserve types.} This renaming can be

  quite cumbersome to reason about. Therefore we made the choice of

  representing a state by a natural number and the states of a Turing

  machine will always consist of the initial segment of natural

  numbers starting from @{text 0} up to the number of states of the

  machine. In doing so we can compose two Turing machine by

  shifting the states of one by an appropriate amount to a higher

  segment and adjusting some ``next states'' in the other.

  An \emph{instruction} @{term i} of a Turing machine is a pair consisting of 

  an action and a natural number (the next state). A \emph{program} @{term p} of a Turing

  machine is then a list of such pairs. Using as an example the following Turing machine

  program, which consists of four instructions

  \begin{equation}

  \begin{tikzpicture}

  \node [anchor=base] at (0,0) {@{thm dither_def}};

  \node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};

  \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};

  \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};

  \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};

  \end{tikzpicture}

  \label{dither}

  \end{equation}

  \noindent

  the reader can see we have organised our Turing machine programs so

  that segments of two belong to a state. The first component of the

  segment determines what action should be taken and which next state

  should be transitioned to in case the head reads a @{term Bk};

  similarly the second component determines what should be done in

  case of reading @{term Oc}. We have the convention that the first

  state is always the \emph{starting state} of the Turing machine.

  The zeroth state is special in that it will be used as the

  ``halting state''.  There are no instructions for the @{text

  0}-state, but it will always perform a @{term Nop}-operation and

  remain in the @{text 0}-state.  Unlike Asperti and Riccioti

  \cite{AspertiRicciotti12}, we have chosen a very concrete

  representation for programs, because when constructing a universal

  Turing machine, we need to define a coding function for programs.

  This can be easily done for our programs-as-lists, but is more

  difficult for the functions used by Asperti and Ricciotti.

  Given a program @{term p}, a state

  and the cell being read by the head, we need to fetch

  the corresponding instruction from the program. For this we define 

  the function @{term fetch}

  \begin{center}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  \multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\

  \end{tabular}

  \end{center}

  \noindent

  In this definition the function @{term nth_of} returns the @{text n}th element

  from a list, provided it exists (@{term Some}-case), or if it does not, it

  returns the default action @{term Nop} and the default state @{text 0} 

  (@{term None}-case). In doing so we slightly deviate from the description

  in \cite{Boolos87}: if their Turing machines transition to a non-existing

  state, then the computation is halted. We will transition in such cases

  to the @{text 0}-state. However, with introducing the

  notion of \emph{well-formed} Turing machine programs we will later exclude such

  cases and make the  @{text 0}-state the only ``halting state''. A program 

  @{term p} is said to be well-formed if it satisfies

  the following three properties:

  \begin{center}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\

                        & @{text "\<and>"} & @{term "iseven (length p)"}\\

                        & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}

  \end{tabular}

  \end{center}

  \noindent

  The first says that @{text p} must have at least an instruction for the starting 

  state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every 

  state, and the third that every next-state is one of the states mentioned in

  the program or being the @{text 0}-state.

  A \emph{configuration} @{term c} of a Turing machine is a state together with 

  a tape. This is written as @{text "(s, (l, r))"}. If we have a 

  configuration and a program, we can calculate

  what the next configuration is by fetching the appropriate action and next state

  from the program, and by updating the state and tape accordingly. 

  This single step of execution is defined as the function @{term tstep}

  \begin{center}

  \begin{tabular}{l}

  @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\

  \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\

  \hspace{10mm}@{text "in (s', update (l, r) a)"}

  \end{tabular}

  \end{center}

  \noindent

  where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is

  empty it returns @{term Bk}.

  It is impossible in Isabelle/HOL to lift the @{term step}-function realising

  a general evaluation function for Turing machines. The reason is that functions in HOL-based

  provers need to be terminating, and clearly there are Turing machine 

  programs that are not. We can however define an evaluation

  function so that it performs exactly @{text n} steps:

  \begin{center}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\

  @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\

  \end{tabular}

  \end{center}

  \noindent

  Recall our definition of @{term fetch} with the default value for

  the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less 

  then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation

  does not actually halt, but rather transitions to the @{text 0}-state and 

  remains there performing @{text Nop}-actions until @{text n} is reached. 

  Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program 

  @{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}

  \begin{center}

  \begin{tabular}{l}

  @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\

  \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}

  \end{tabular}

  \end{center}

  \noindent

  where @{text 1} stands for the starting state and @{text 0} for our final state.

  A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff

  \begin{center}

  @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>

  \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}

  \end{center}

  \noindent

  Later on we need to consider specific Turing machines that 

  start with a tape in standard form and halt the computation

  in standard form. To define a tape in standard form, it is

  useful to have an operation %@{ term "tape_of_nat_list DUMMY"} 

  that translates lists of natural numbers into tapes. 

  \begin{center}

  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\

  %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\

  %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\

  \end{tabular}

  \end{center}

  By this we mean

  \begin{center}

  %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}

  \end{center}

  \noindent

  This means the Turing machine starts with a tape containg @{text n} @{term Oc}s

  and the head pointing to the first one; the Turing machine

  halts with a tape consisting of some @{term Bk}s, followed by a 

  ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.

  The head in the output is pointing again at the first @{term Oc}.

  The intuitive meaning of this definition is to start the Turing machine with a

  tape corresponding to a value @{term n} and producing

  a new tape corresponding to the value @{term l} (the number of @{term Oc}s

  clustered on the output tape).

  Before we can prove the undecidability of the halting problem for Turing machines, 

  we have to define how to compose two Turing machines. Given our setup, this is 

  relatively straightforward, if slightly fiddly. We use the following two

  auxiliary functions: