(*<*)

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

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

``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 tilings---in 

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 complete formalisation of Turing

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

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 

functions. 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 Turing 

machine uses a different alphabet than the machines it simulates. They

\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}

where Turing machines (and our

universal Turing machine) operates on tapes that contain only blank

or filled cells (respectively represented by 0 and 1---or in our 

\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

(*>*)