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