(*<*)+
−
theory Paper+
−
imports UTM+
−
begin+
−
+
−
declare [[show_question_marks = false]]+
−
(*>*)+
−
+
−
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. The reason is that both algorithms are formulated in terms+
−
of inductive predicates. Suppose @{text "P"} stands for one such+
−
predicate.  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, since it is a theorem prover 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. 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 the HOL4 theorem prover. He choose the+
−
$\lambda$-calculus as the starting point for his formalisation+
−
of computability theory,+
−
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 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}+
−
+
−
\noindent+
−
In this paper we took 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 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+
−
in theorem provers 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 definition is a set of states+
−
together with a transition function, both 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 lengthy and detailed 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 that use them. We give as+
−
example one proof---undecidability of Wang tilings---in Section+
−
\ref{Wang}. The standard proof of this property uses the notion of+
−
\emph{universal Turing machines}.+
−
+
−
We are not the first who formalised Turing machines in a theorem+
−
prover: we are aware of the preliminary work by Asperti and Ricciotti+
−
\cite{AspertiRicciotti12}. They describe a formalisation of Turing+
−
machines in the Matita theorem prover. They report +
−
that the informal proofs from which they started are not +
−
``sufficiently accurate to be directly used as a guideline for +
−
formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation +
−
we followed the proofs from the textbook \cite{Boolos87} and found that the description+
−
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 generalize 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 +
−
function. But the general ideas for how to do this are clear enough in +
−
\cite{Boolos87}.+
−
+
−
The main difference between our formalisation and the one by Asperti and+
−
Ricciotti is +
−
+
−
that their universal machines +
−
+
−
\begin{quote}+
−
``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+
−
{\bf Contributions:} +
−
+
−
*}+
−
+
−
section {* Formalisation *}+
−
+
−
text {*+
−
  +
−
*}+
−
+
−
+
−
section {* Wang Tiles\label{Wang} *}+
−
+
−
text {*+
−
  Used in texture mapings - graphics+
−
*}+
−
+
−
+
−
section {* Related Work *}+
−
+
−
text {*+
−
  The most closely related work is by Norrish. He 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+
−
(*>*)+
−