1 (*<*)

     2 theory Paper

     3 imports UTM

     4 begin

     5 

     6 declare [[show_question_marks = false]]

     7 (*>*)

     8 

     9 section {* Introduction *}

    10 

    11 text {*

    12 

    13 In earlier work, we formalised in Isabelle/HOL the correctness 

    14 proofs for two algorithms, one about type-checking in LF and 

    15 another about deciding requests in access control [???]. These 

    16 formalisation efforts uncovered a gap in the informal correctness 

    17 proof of the former and made us realise that important details 

    18 were left out in the informal model for the latter. However, 

    19 in both cases we were unable to formalise computablility 

    20 arguments. The reason is that both algorithms are formulated

    21 as inductive predicates. Say @{text "P"} is one such predicate.

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

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

    24 since it is a theorem prover based on classical logic where

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

    26 always provable.   

    27 

    28 

    29 

    30 

    31 These algorithms

    32 were given as inductively defined predicates.  

    33 inductively defined predicates, but 

    34 

    35 

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

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

    38  

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

    40 

    41 

    42 Our formalisation follows XXX

    43 

    44 \noindent

    45 {\bf Contributions:} 

    46 

    47 *}

    48 

    49 section {* Related Work *}

    50 

    51 text {*

    52   The most closely related work is by Norrish. He bases his approach on 

    53   lambda-terms. For this he introduced a clever rewriting technology

    54   based on combinators and de-Bruijn indices for

    55   rewriting modulo $\beta$-equivalence (to keep it manageable)

    56 *}

    57 

    58 

    59 (*

    60 Questions:

    61 

    62 Can this be done: Ackerman function is not primitive 

    63 recursive (Nora Szasz)

    64 

    65 Tape is represented as two lists (finite - usually infinite tape)?

    66 

    67 *)

    68 

    69 

    70 (*<*)

    71 end

    72 (*>*)