(*<*)theory Paperimports UTMbegindeclare [[show_question_marks = false]](*>*)section {* Introduction *}text {*\noindentWe formalised in earlier work the correctness proofs for twoalgorithms in Isabelle/HOL---one about type-checking inLF~\cite{UrbanCheneyBerghofer11} and another about deciding requestsin access control~\cite{WuZhangUrban12}. The formalisationsuncovered a gap in the informal correctness proof of the former andmade us realise that important details were left out in the informalmodel for the latter. However, in both cases we were unable toformalise in Isabelle/HOL computability arguments about thealgorithms. The reason is that both algorithms are formulated in termsof inductive predicates. Suppose @{text "P"} stands for one suchpredicate. Decidability of @{text P} usually amounts to showingwhether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} workin Isabelle/HOL, since it is a theorem prover based on classical logicwhere the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}is always provable no matter whether @{text P} is constructed bycomputable means. The same problem would arise if we had formulatedthe algorithms as recursive functions, because internally inIsabelle/HOL, like in all HOL-based theorem provers, functions arerepresented as inductively defined predicates too.The only satisfying way out of this problem in a theorem prover based on classicallogic is to formalise a theory of computability. Norrish provided sucha formalisation for the HOL4 theorem prover. He choose the$\lambda$-calculus as the starting point for his formalisationof computability theory,because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of hisformalisation is a clever infrastructure for reducing$\lambda$-terms. He also established the computational equivalencebetween the $\lambda$-calculus and recursive functions. Nevertheless heconcluded that it would be ``appealing'' to have formalisations for moreoperational models of computations, such as Turing machines or registermachines. One reason is that many proofs in the literature use them. He noted however that in the context of theorem provers\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}\noindentIn this paper we took on this daunting prospect and provide aformalisation of Turing machines, as well as abacus machines (a kindof register machines) and recursive functions. To see the difficultiesinvolved with this work, one has to understand that interactivetheorem provers, like Isabelle/HOL, are at their best when thedata-structures at hand are ``structurally'' defined, like lists,natural numbers, regular expressions, etc. Such data-structures comewith convenient reasoning infrastructures (for example inductionprinciples, recursion combinators and so on). But this is \emph{not}the case with Turing machines (and also not with register machines):underlying their definition is a set of states together with atransition function, both of which are not structurally defined. Thismeans we have to implement our own reasoning infrastructure in orderto prove properties about them. This leads to annoyingly fiddlyformalisations. We noticed first the difference between both,structural and non-structural, ``worlds'' when formalising theMyhill-Nerode theorem, where regular expressions fared much betterthan automata \cite{WuZhangUrban11}. However, with Turing machinesthere seems to be no alternative if one wants to formalise the greatmany proofs from the literature that use them. We will analyse oneexample---undecidability of Wang tilings---in Section~\ref{Wang}. Thestandard proof of this property uses the notion of \emph{universalTuring machines}.We are not the first who formalised Turing machines in a theoremprover: we are aware of the preliminary work by Asperti and Ricciotti\cite{AspertiRicciotti12}. They describe a complete formalisation ofTuring machines in the Matita theorem prover, including a universalTuring machine. They report that the informal proofs from which theystarted are not ``sufficiently accurate to be directly used as aguideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. Forour formalisation we followed the proofs from the textbook\cite{Boolos87} and found that the description there is quitedetailed. Some details are left out however: for example, it is onlyshown how the universal Turing machine is constructed for Turingmachines computing unary functions. We had to figure out a way togeneralize this result to $n$-ary functions. Similarly, when compilingrecursive functions to abacus machines, the textbook again only showshow it can be done for 2- and 3-ary functions, but in theformalisation we need arbitrary functions. But the general ideas forhow to do this are clear enough in \cite{Boolos87}. However, oneaspect that is completely left out from the informal description in\cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turingmachines are correct. We will introduce Hoare-style proof ruleswhich help us with such correctness arguments of Turing machines.The main difference between our formalisation and the one by Aspertiand Ricciotti is that their universal Turing machine uses a differentalphabet than the machines it simulates. They write \cite[Page23]{AspertiRicciotti12}:\begin{quote}\it``In particular, the fact that the universal machine operates with adifferent alphabet with respect to the machines it simulates isannoying.'' \end{quote}\noindentIn this paper we follow the approach by Boolos et al \cite{Boolos87},which goes back to Post \cite{Post36}, where all Turing machinesoperate on tapes that contain only blank or filled cells (represented by @{term Bk} and @{term Oc}, respectively, in ourformalisation). Traditionally the content of a cell can be anycharacter from a finite alphabet. Although computationallyequivalennt, the more restrictive notion of Turing machines makethe reasoning more uniform. Unfortunately, it also makes itharder to design programs for Turing machines. Thereforein order to construct a \emph{universal Turing machine} we followthe proof in \cite{Boolos87} by relating abacus machines toturing machines and in turn recursive functions to abacus machines. \medskip\noindent{\bf Contributions:} *}section {* Turing Machines *}text {* Tapes %\begin{center} %\begin{tikzpicture} %% %\end{tikzpicture} %\end{center} An action is defined as \begin{center} \begin{tabular}{rcll} @{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\\ \end{tabular} \end{center} For showing the undecidability of the halting problem, we need to consider two specific Turing machines.*}section {* Abacus Machines *}section {* Recursive Functions *}section {* Wang Tiles\label{Wang} *}text {* Used in texture mapings - graphics*}section {* Related Work *}text {* The most closely related work is by Norrish \cite{Norrish11}, and Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on lambda-terms. For this he introduced a clever rewriting technology based on combinators and de-Bruijn indices for rewriting modulo $\beta$-equivalence (to keep it manageable)*}(*Questions:Can this be done: Ackerman function is not primitive recursive (Nora Szasz)Tape is represented as two lists (finite - usually infinite tape)?*)(*<*)end(*>*)