(*<*)

theory Paper

imports UTM

begin

declare [[show_question_marks = false]]

(*>*)

section {* Introduction *}

text {*

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 computablility 

Decidability of @{text P} usually amounts to showing whether 

@{term "P \<or> \<not>P"} holds. But this does not work in Isabelle/HOL,

since it is a theorem prover based on classical logic where

the law of excluded midle ensures that @{term "P \<or> \<not>P"} is 

always provable.   

These algorithms

were given as inductively defined predicates.  

inductively defined predicates, but 

Norrish choose the $\lambda$-calculus as a starting point

for his formalisation, because of its ``simplicity'' [Norrish]

``Turing machines are an even more daunting prospect'' [Norrish]

Our formalisation follows XXX

\noindent

{\bf Contributions:} 

*}

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

(*>*)