(*<*)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.The only satisfying way out is to formalise a theory ofcomputability. Norrish provided such a formalisation for the HOL4theorem prover. He choose the $\lambda$-calculus as the starting pointfor his formalisation, because of its ``simplicity'' \cite[Page297]{Norrish11}. Part of his formalisation is a clever infrastructurefor reducing $\lambda$-terms. He also established the computationalequivalence between the lambda-calculus and recursive functions.Nevertheless he concluded that it would be appealing to haveformalisations of more operational models of computations such asTuring machines or register machines. One reason is that many proofsin the literature refer to them. He noted however that in the contextof 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 \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(*>*)