(*<*)+ −
theory Paper+ −
imports UTM+ −
begin+ −
+ −
declare [[show_question_marks = false]]+ −
(*>*)+ −
+ −
section {* Introduction *}+ −
+ −
text {*+ −
+ −
We formalised in earlier work the correctness + −
proofs for two algorithms in Isabelle/HOL, one about type-checking in LF and + −
another about deciding requests in access control \cite{UrbanCheneyBerghofer11} [???]: + −
these + −
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 computablility + −
arguments for 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 + −
@{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 {* 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+ −
(*>*)+ −