(*<*)

theory Paper

imports "../thys/abacus"

begin

(*

hide_const (open) s 

*)

hide_const (open) Divides.adjust

abbreviation

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

consts DUMMY::'a

(* THEOREMS *)

notation (Rule output)

  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

syntax (Rule output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

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

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 

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

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (Axiom output)

  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

notation (IfThen output)

  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

syntax (IfThen output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (IfThenNoBox output)

  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

syntax (IfThenNoBox output)

  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("_")

context uncomputable

begin

notation (latex output)

  Cons ("_::_" [48,47] 48) and

  set ("") and

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

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

  update2 ("update") and

  tm_wf0 ("wf") and

  (*is_even ("iseven") and*)

  tcopy_begin ("cbegin") and

  tcopy_loop ("cloop") and

  tcopy_end ("cend") and

  step0 ("step") and

  tcontra ("contra") and

  code_tcontra ("code contra") and

  steps0 ("steps") and

  exponent ("_\<^bsup>_\<^esup>") and

  haltP ("halts") and 

  tcopy ("copy") and 

  tape_of ("\<langle>_\<rangle>") and 

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

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

  inv_begin0 ("I\<^isub>0") and

  inv_begin1 ("I\<^isub>1") and

  inv_begin2 ("I\<^isub>2") and

  inv_begin3 ("I\<^isub>3") and

  inv_begin4 ("I\<^isub>4") and 

  inv_begin ("I\<^bsub>cbegin\<^esub>") and

  inv_loop1 ("J\<^isub>1") and

  inv_loop0 ("J\<^isub>0") and

  inv_end1 ("K\<^isub>1") and

  inv_end0 ("K\<^isub>0") and

  measure_begin_step ("M\<^bsub>cbegin\<^esub>")

lemma inv_begin_print:

  shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and

        "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 

        "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and 

        "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and 

        "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and

        "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"

apply(case_tac [!] tp)

by (auto)

lemma inv1: 

  shows "0 < n \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"

unfolding assert_imp_def

unfolding inv_loop1.simps inv_begin0.simps

apply(auto)

apply(rule_tac x="1" in exI)

apply(auto simp add: replicate.simps)

done

lemma inv2: 

  shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"

apply(rule ext)

apply(case_tac x)

apply(simp add: inv_end1.simps)

done

lemma measure_begin_print:

  shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and

        "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and

        "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 

        "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"

by (simp_all)

declare [[show_question_marks = false]]

lemma nats2tape:

  shows "<([]::nat list)> = []"

  and "<[n]> = <n>"

  and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"

  and "<(n, m)> = <n> @ [Bk] @ <m>"

  and "<[n, m]> = <(n, m)>"

  and "<n> = Oc \<up> (n + 1)" 

apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)

apply(case_tac ns)

apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)

done 

lemmas HR1 = 

  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]

lemmas HR2 =

  Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]

lemma inv_begin01:

  assumes "n > 1"

  shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"

using assms by auto                          

lemma inv_begin02:

  assumes "n = 1"

  shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"

using assms by auto

(*>*)

section {* Introduction *}

text {*

%\noindent

%We formalised in earlier work the correctness proofs for two

%algorithms in Isabelle/HOL---one about type-checking in

%LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests

%in access control~\cite{WuZhangUrban12}.  The formalisations

%uncovered a gap in the informal correctness proof of the former and

%made us realise that important details were left out in the informal

%model for the latter. However, in both cases we were unable to

%formalise in Isabelle/HOL computability arguments about the

%algorithms. 

\noindent

Suppose you want to mechanise a proof for whether a predicate @{term

P}, say, is decidable or not. Decidability of @{text P} usually

amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this

does \emph{not} work in Isabelle/HOL and other HOL theorem provers,

since they are based on classical logic 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 computable means. We hit on

this limitation previously when we mechanised the correctness proofs

of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but

were unable to formalise arguments about decidability or undecidability.

%The same problem would arise if we had formulated

%the algorithms as recursive functions, because internally in

%Isabelle/HOL, like in all HOL-based theorem provers, functions are

%represented as inductively defined predicates too.

The only satisfying way out of this problem in a theorem prover based

on classical logic is to formalise a theory of computability. Norrish

provided such a formalisation for HOL4. He choose the

$\lambda$-calculus as the starting point for his formalisation because

of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his

formalisation is a clever infrastructure for reducing

$\lambda$-terms. He also established the computational equivalence

between the $\lambda$-calculus and recursive functions.  Nevertheless

he concluded that it would be appealing to have formalisations for

more operational models of computations, such as Turing machines or

register machines.  One reason is that many proofs in the literature

use them.  He noted however that \cite[Page 310]{Norrish11}:

\begin{quote}

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

general fiddliness,\\ Turing machines are an even more 

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

involved with this work, one has to understand that Turing machine

programs can be completely \emph{unstructured}, behaving similar to

Basic programs involving the infamous goto \cite{Dijkstra68}. This

precludes in the general case a compositional Hoare-style reasoning

about Turing programs.  We provide such Hoare-rules for when it

\emph{is} possible to reason in a compositional manner (which is

fortunately quite often), but also tackle the more complicated case

when we translate abacus programs into Turing programs.  This

reasoning about concrete Turing machine programs is usually

left out in the informal literature, e.g.~\cite{Boolos87}.

%To see the difficulties

%involved with this work, one has to understand that interactive

%theorem provers, like Isabelle/HOL, are at their best when the

%data-structures at hand are ``structurally'' defined, like lists,

%natural numbers, regular expressions, etc. Such data-structures come

%with convenient reasoning infrastructures (for example induction

%principles, recursion combinators and so on).  But this is \emph{not}

%the case with Turing machines (and also not with register machines):

%underlying their definitions are sets of states together with 

%transition functions, all of which are not structurally defined.  This

%means we have to implement our own reasoning infrastructure in order

%to prove properties about them. This leads to annoyingly fiddly

%formalisations.  We noticed first the difference between both,

%structural and non-structural, ``worlds'' when formalising the

%Myhill-Nerode theorem, where regular expressions fared much better

%than automata \cite{WuZhangUrban11}.  However, with Turing machines

%there seems to be no alternative if one wants to formalise the great

%many proofs from the literature that use them.  We will analyse one

%example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The

%standard proof of this property uses the notion of universal

%Turing machines.

We are not the first who formalised Turing machines: we are aware of

the work by Asperti and Ricciotti \cite{AspertiRicciotti12}. They

describe a complete formalisation of Turing machines in the Matita

theorem prover, including a universal Turing machine. However, they do

\emph{not} formalise the undecidability of the halting problem since

their main focus is complexity, rather than computability theory. They

also report that the informal proofs from which they started are not

``sufficiently accurate to be directly usable as a guideline for

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

formalisation we follow mainly the proofs from the textbook by Boolos

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

detailed. Some details are left out however: for example, constructing

the \emph{copy Turing machine} is left as an excerise to the

reader---a correctness proof is not mentioned at all; also \cite{Boolos87}

only shows 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

how to do this are clear enough in \cite{Boolos87}.

%However, one

%aspect that is completely left out from the informal description in

%\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing

%machines are correct. We will introduce Hoare-style proof rules

%which help us with such correctness arguments of Turing machines.

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. 

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 translating 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.  

For reasoning about Turing machine programs we derive Hoare-rules.

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

translating 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 other

results: we describe a proof of the computational equivalence

of single-sided Turing machines, which is not given in \cite{Boolos87},

but needed for example for formalising the undecidability proof of 

Wang's tiling problem \cite{Robinson71}.

%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 \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 use

  the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists

  composed of @{term n} elements of @{term Bk}s.  We also 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

  scannes. This can be pictured as follows:

  %

  \begin{center}

  \begin{tikzpicture}[scale=0.9]

  \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[fill]     (-1.65,0.1) rectangle (-1.35,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.85,-0.5) {\small left list};

  \node [anchor=base] at (0.40,-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}

  \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}

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

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

  \end{tabular}

  \begin{tabular}[t]{rcl@ {\hspace{2mm}}l}

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

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

  \end{tabular}

  \begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}

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

  \end{tabular}

  \end{center}

  \noindent

  We slightly deviate

  from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12}) 

  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(3)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(3)}\\

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

  @{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

  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.

  %Note that our treatment of the tape is rather ``unsymmetric''---we

  %have the convention that the head of the right list is where the

  %head is currently positioned. Asperti and Ricciotti

  %\cite{AspertiRicciotti12} also considered such a representation, but

  %dismiss it as it complicates their definition for \emph{tape

  %equality}. The reason is that moving the head one step to

  %the left and then back to the right might change the tape (in case

  %of going over the ``edge''). Therefore they distinguish four types

  %of tapes: one where the tape is empty; another where the head

  %is on the left edge, respectively right edge, and in the middle

  %of the tape. The reading, writing and moving of the tape is then

  %defined in terms of these four cases.  In this way they can keep the

  %tape in a ``normalised'' form, and thus making a left-move followed

  %by a right-move being the identity on tapes. Since we are not using

  %the notion of tape equality, we can get away with the unsymmetric

  %definition above, and by using the @{term update} function

  %cover uniformly all cases including corner cases.

  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. 

  We follow the choice made in \cite{AspertiRicciotti12} 

  by representing a state with a natural number and the states in a Turing

  machine program by the initial segment of natural numbers starting from @{text 0}.

  In doing so we can compose two Turing machine programs 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} 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.64) 

  {$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm] 

  = starting state\end{tabular}}}$};

  \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 such a

  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 @{text 0}-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