(*<*)

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 

\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

(*>*)