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

The only satisfying way out 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, 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 of more operational models of computations such as
Turing machines or register machines.  One reason is that many proofs
in the literature refer to 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 





\cite{AspertiRicciotti12}


Our formalisation follows XXX

\noindent
{\bf Contributions:} 

*}


section {* Wang Tiles *}

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