--- 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,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l}
+ A \emph{standard tape} is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} 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 \<up>"}
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' \<mapsto> 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 "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (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.
--- 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,