--- a/Paper/Paper.thy Sun Jan 27 14:57:54 2013 +0000
+++ b/Paper/Paper.thy Sun Jan 27 15:46:32 2013 +0000
@@ -177,8 +177,10 @@
of the preliminary work by Asperti and Ricciotti
\cite{AspertiRicciotti12}. They describe a complete formalisation of
Turing machines in the Matita theorem prover, including a universal
-Turing machine. They report that the informal proofs from which they
-started are \emph{not} ``sufficiently accurate to be directly usable as a
+Turing machine. However, they do \emph{not} formalise the undecidability of the
+halting problem since their main focus is complexity, rather than
+computability theory. They 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
@@ -520,7 +522,9 @@
halts, then in our setting the @{term steps}-evaluation does not
actually halt, but rather transitions to the @{text 0}-state (the
final state) and remains there performing @{text Nop}-actions until
- @{text n} is reached.
+ @{text n} is reached. This is different from the setup in
+ \cite{AspertiRicciotti12} where an option is returned once a final
+ state is reached.
\begin{figure}[t]
\begin{center}
@@ -674,7 +678,9 @@
whose three components are given in Figure~\ref{copy}. To the prove
correctness of these Turing machine programs, we introduce the
notion of total correctness defined in terms of
- \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the
+ \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar
+ to the notion of \emph{realisability} in \cite{AspertiRicciotti12}.
+ They implement the
idea that a program @{term 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
@@ -703,19 +709,28 @@
\end{center}
\noindent
- We have set up our Hoare-style reasoning so that we can deal explicitly
- with total correctness and non-terminantion, rather than have notions for partial
- correctness and termination. Although the latter would allow us to reason
- more uniformly (only using Hoare-triples), we prefer our definitions because
- we can derive simple Hoare-rules for sequentially composed Turing programs.
- In this way we can reason about the correctness of @{term "tcopy_init"},
- for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}.
+ Like Asperti and Ricciotti with their notion of realisability, we
+ have set up our Hoare-style reasoning so that we can deal explicitly
+ with total correctness and non-terminantion, rather than have
+ notions for partial correctness and termination. Although the latter
+ would allow us to reason more uniformly (only using Hoare-triples),
+ we prefer our definitions because we can derive (below) simple
+ Hoare-rules for sequentially composed Turing programs. In this way
+ we can reason about the correctness of @{term "tcopy_init"}, for
+ example, completely separately from @{term "tcopy_loop"} and @{term
+ "tcopy_end"}.
+
+ It is realatively straightforward to prove that the Turing program
+ @{term "dither"} shown in \eqref{dither} is correct. This program
+ should be the ``identity'' when started with a standard tape representing
+ @{text "1"} but loop when started with @{text 0} instead.
+
\begin{center}
\begin{tabular}{l@ {\hspace{3mm}}lcl}
& \multicolumn{1}{c}{start tape}\\[1mm]
- \raisebox{2.5mm}{halting case:} &
- \begin{tikzpicture}[scale=0.9]
+ \raisebox{2mm}{halting case:} &
+ \begin{tikzpicture}[scale=0.8]
\draw[very thick] (-2,0) -- ( 0.75,0);
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
@@ -728,8 +743,8 @@
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}
- & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} &
- \begin{tikzpicture}[scale=0.9]
+ & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
+ \begin{tikzpicture}[scale=0.8]
\draw[very thick] (-2,0) -- ( 0.75,0);
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
@@ -743,8 +758,8 @@
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}\\
- \raisebox{2.5mm}{non-halting case:} &
- \begin{tikzpicture}[scale=0.9]
+ \raisebox{2mm}{non-halting case:} &
+ \begin{tikzpicture}[scale=0.8]
\draw[very thick] (-2,0) -- ( 0.25,0);
\draw[very thick] (-2,0.5) -- ( 0.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
@@ -755,15 +770,14 @@
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}
- & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} &
- \raisebox{2.5mm}{loops}
+ & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
+ \raisebox{2mm}{loops}
\end{tabular}
\end{center}
-
- It is straightforward to prove that the Turing program
- @{term "dither"} satisfies the following correctness properties
-
+ \noindent
+ We can prove the following formal statements
+
\begin{center}
\begin{tabular}{l}
@{thm dither_halts}\\