# HG changeset patch # User Christian Urban # Date 1359632116 0 # Node ID 01f688735b9b704288d3d7f6c2c1aeb519956d66 # Parent 294576baaeedb9800e18032a3b6e547288a0f8f9 updated paper diff -r 294576baaeed -r 01f688735b9b Paper/Paper.thy --- a/Paper/Paper.thy Wed Jan 30 23:57:33 2013 +0000 +++ b/Paper/Paper.thy Thu Jan 31 11:35:16 2013 +0000 @@ -235,18 +235,18 @@ also report that the informal proofs from which they started are not ``sufficiently accurate to be directly usable as a guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For our -formalisation we follow mainly the proofs from the textbook -\cite{Boolos87} and found that the description there is quite +formalisation we follow mainly the proofs from the textbook by Boolos +et al \cite{Boolos87} and found that the description there is quite detailed. Some details are left out however: for example, constructing -the \emph{copy Turing machine} and its correctness proof are left as -an excerise to the reader; also \cite{Boolos87} only shows how the -universal Turing machine is constructed for Turing machines computing -unary functions. We had to figure out a way to generalise this result -to $n$-ary functions. Similarly, when compiling recursive functions to -abacus machines, the textbook again only shows how it can be done for -2- and 3-ary functions, but in the formalisation we need arbitrary -functions. But the general ideas for how to do this are clear enough -in \cite{Boolos87}. +the \emph{copy Turing machine} is left as an excerise to the +reader---a correctness proof is not mentioned at all; also \cite{Boolos87} +only shows how the universal Turing machine is constructed for Turing +machines computing unary functions. We had to figure out a way to +generalise this result to $n$-ary functions. Similarly, when compiling +recursive functions to abacus machines, the textbook again only shows +how it can be done for 2- and 3-ary functions, but in the +formalisation we need arbitrary functions. But the general ideas for +how to do this are clear enough in \cite{Boolos87}. %However, one %aspect that is completely left out from the informal description in %\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing @@ -555,13 +555,13 @@ \end{center} \noindent - where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is - empty it returns @{term Bk}. - It is impossible in Isabelle/HOL to lift the @{term step}-function to realise - a general evaluation function for Turing machines. The reason is that functions in HOL-based - provers need to be terminating, and clearly there are Turing machine - programs that are not. We can however define an evaluation - function that performs exactly @{text n} steps: + where @{term "read r"} returns the head of the list @{text r}, or if + @{text r} is empty it returns @{term Bk}. It is impossible in + Isabelle/HOL to lift the @{term step}-function in order to realise a + general evaluation function for Turing machines programs. The reason + is that functions in HOL-based provers need to be terminating, and + clearly there are programs that are not. We can however define a + recursive evaluation function that performs exactly @{text n} steps: \begin{center} \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} @@ -694,10 +694,11 @@ \end{figure} - We often need to restrict tapes to be in \emph{standard form}, which means + We often need to restrict tapes to be in standard form, which means the left list of the tape is either empty or only contains @{text "Bk"}s, and the right list contains some ``clusters'' of @{text "Oc"}s separted by single blanks. To make this formal we define the following overloaded function + encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s. \begin{center} \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @@ -712,18 +713,19 @@ \end{center} \noindent - A standard tape is then of the form @{text "(Bk\<^isup>l,\[n\<^isub>1,...,n\<^isub>m]\)"} for some @{text l} + A \emph{standard tape} is then of the form @{text "(Bk\<^isup>l,\[n\<^isub>1,...,n\<^isub>m]\)"} for some @{text l} and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0} is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on. - Before we can prove the undecidability of the halting problem for our - Turing machines, we have to analyse two concrete Turing machine - programs and establish that they are correct---that means they are - ``doing what they are supposed to be doing''. Such correctness proofs are usually left - out in the informal literature, for example \cite{Boolos87}. The first program - we need to prove correct is the @{term dither} program shown in \eqref{dither} - and the second program is @{term "tcopy"} defined as + Before we can prove the undecidability of the halting problem for + our Turing machines working on standard tapes, we have to analyse + two concrete Turing machine programs and establish that they are + correct---that means they are ``doing what they are supposed to be + doing''. Such correctness proofs are usually left out in the + informal literature, for example \cite{Boolos87}. The first program + we need to prove correct is the @{term dither} program shown in + \eqref{dither} and the second program is @{term "tcopy"} defined as \begin{equation} \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @@ -739,7 +741,7 @@ p} started in state @{term "1::nat"} with a tape satisfying @{term P} will after some @{text n} steps halt (have transitioned into the halting state) with a tape satisfying @{term Q}. This idea is very - similar to \emph{realisability} in \cite{AspertiRicciotti12}. We + similar to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \"} implementing the case that a program @{term p} started with a tape satisfying @{term P} will loop (never transition into the halting @@ -771,8 +773,11 @@ @{thm[mode=Rule] Hoare_consequence} \end{equation} + \noindent + where + @{term "P' \ P"} stands for the fact that for all tapes @{term "tp"}, + @{term "P' tp"} implies @{term "P tp"}. - \noindent Like Asperti and Ricciotti with their notion of realisability, we have set up our Hoare-rules so that we can deal explicitly with total correctness and non-terminantion, rather than have @@ -855,8 +860,8 @@ number of steps we can perform starting from the input tape. The program @{term tcopy} defined in \eqref{tcopy} has 15 states; - its purpose is to produce the standard tape @{term "(DUMMY, <(n, - n::nat)>)"} when started with @{term "(DUMMY, <(n::nat)>)"}, that is + its purpose is to produce the standard tape @{term "(Bks, <(n, + n::nat)>)"} when started with @{term "(Bks, <(n::nat)>)"}, that is making a copy of a value on the tape. Reasoning about this program is substantially harder than about @{term dither}. To ease the burden, we derive the following two Hoare-rules for sequentially @@ -889,11 +894,11 @@ "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in isolation. We will show the details for the program @{term "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, - @{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to + @{term "inv_begin4"} shown in Figure~\ref{invbegin}, which correspond to each state of @{term tcopy_begin}, we define the following invariant for the whole @{term tcopy_begin} program: - \begin{figure} + \begin{figure}[t] \begin{center} \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}} @{thm (lhs) inv_begin0.simps} & @{text "\"} & @{thm (rhs) inv_begin01} @{text "\"}& (halting state)\\ @@ -925,9 +930,10 @@ \noindent This invariant depends on @{term n} representing the number of - @{term Oc}s on the tape. It is not hard (26 lines of automated proof - script) to show that for @{term "n > (0::nat)"} this invariant is - preserved under computation rules @{term step} and @{term steps}. + @{term Oc}s (or encoded number) on the tape. It is not hard (26 + lines of automated proof script) to show that for @{term "n > + (0::nat)"} this invariant is preserved under computation rules + @{term step} and @{term steps}. measure for the copying TM, which we however omit. diff -r 294576baaeed -r 01f688735b9b Paper/document/root.bib --- a/Paper/document/root.bib Wed Jan 30 23:57:33 2013 +0000 +++ b/Paper/document/root.bib Thu Jan 31 11:35:16 2013 +0000 @@ -32,9 +32,10 @@ @Unpublished{WuZhangUrban12, author = {C.~Wu and X.~Zhang and C.~Urban}, - title = {???}, + title = {{A} {F}ormal {M}odel and {C}orrectness {P}roof for an + {A}ccess {C}ontrol {P}olicy {F}ramework}, note = {Submitted}, - year = {2012} + year = {2013} } @book{Boolos87, diff -r 294576baaeed -r 01f688735b9b paper.pdf Binary file paper.pdf has changed