# HG changeset patch # User Christian Urban # Date 1356902319 0 # Node ID c216ae455c90f8306d4facdf37b8a3e7c8487ce8 # Parent f7896d90aa19af1cf725b11cc465c6af88c54cf8 more on the paper diff -r f7896d90aa19 -r c216ae455c90 Paper.thy --- a/Paper.thy Sun Dec 30 14:58:48 2012 +0000 +++ b/Paper.thy Sun Dec 30 21:18:39 2012 +0000 @@ -10,34 +10,54 @@ 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 \ \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 \ \P"} is -always provable. +\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 \ \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 \ \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 -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] +\cite{AspertiRicciotti12} Our formalisation follows XXX diff -r f7896d90aa19 -r c216ae455c90 document/root.bib --- a/document/root.bib Sun Dec 30 14:58:48 2012 +0000 +++ b/document/root.bib Sun Dec 30 21:18:39 2012 +0000 @@ -7,3 +7,33 @@ year = {2011}, pages = {15:1--15:42} } + +@inproceedings{Norrish11, + author = {M.~Norrish}, + title = {{M}echanised {C}omputability {T}heory}, + booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving (ITP)}, + year = {2011}, + series = {LNCS}, + volume = {6898}, + pages = {297--311} +} + +@inproceedings{AspertiRicciotti12, + author = {A.~Asperti and W.~Ricciotti}, + title = {{F}ormalizing {T}uring {M}achines}, + booktitle = {Proc.~of the 19th International Workshop on Logic, Language, + Information and Computation (WoLLIC)}, + year = {2012}, + pages = {1-25}, + series = {LNCS}, + volume = {7456} +} + + +@Unpublished{WuZhangUrban12, + author = {C.~Wu and X.~Zhang and C.~Urban}, + title = {???}, + note = {Submitted}, + year = {2012} +} + diff -r f7896d90aa19 -r c216ae455c90 document/root.tex --- a/document/root.tex Sun Dec 30 14:58:48 2012 +0000 +++ b/document/root.tex Sun Dec 30 21:18:39 2012 +0000 @@ -1,26 +1,8 @@ \documentclass[10pt, conference, compsocconf]{IEEEtran} -\usepackage{isabelle,isabellesym} - -%\usepackage{amssymb} - %for \, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage[greek,english]{babel} - %option greek for \ - %option english (default language) for \, \ - -%\usepackage[only,bigsqcap]{stmaryrd} - %for \ - -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \, \, \, \, - %\ - -% this should be the last package used +\usepackage{isabelle} +\usepackage{isabellesym} +\usepackage{times} +\usepackage{amssymb} \usepackage{mathpartir} \usepackage{pdfsetup} @@ -67,15 +49,6 @@ \IEEEpeerreviewmaketitle - -%\tableofcontents - -% sane default for proof documents -\parindent 0pt\parskip 0.5ex - - - - % generated text of all theories \input{session} diff -r f7896d90aa19 -r c216ae455c90 paper.pdf Binary file paper.pdf has changed