# HG changeset patch # User Christian Urban # Date 1359301592 0 # Node ID d2f4b775cd150ced3b539446c932c34d76657c35 # Parent c67e8ed4c865cb080039fdc8fa75d9c0167ee0fb updated paper diff -r c67e8ed4c865 -r d2f4b775cd15 Paper/Paper.thy --- 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}\\ diff -r c67e8ed4c865 -r d2f4b775cd15 paper.pdf Binary file paper.pdf has changed