175 |
175 |
176 We are not the first who formalised Turing machines: we are aware |
176 We are not the first who formalised Turing machines: we are aware |
177 of the preliminary work by Asperti and Ricciotti |
177 of the preliminary work by Asperti and Ricciotti |
178 \cite{AspertiRicciotti12}. They describe a complete formalisation of |
178 \cite{AspertiRicciotti12}. They describe a complete formalisation of |
179 Turing machines in the Matita theorem prover, including a universal |
179 Turing machines in the Matita theorem prover, including a universal |
180 Turing machine. They report that the informal proofs from which they |
180 Turing machine. However, they do \emph{not} formalise the undecidability of the |
181 started are \emph{not} ``sufficiently accurate to be directly usable as a |
181 halting problem since their main focus is complexity, rather than |
|
182 computability theory. They also report that the informal proofs from which they |
|
183 started are not ``sufficiently accurate to be directly usable as a |
182 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
184 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
183 our formalisation we follow mainly the proofs from the textbook |
185 our formalisation we follow mainly the proofs from the textbook |
184 \cite{Boolos87} and found that the description there is quite |
186 \cite{Boolos87} and found that the description there is quite |
185 detailed. Some details are left out however: for example, constructing |
187 detailed. Some details are left out however: for example, constructing |
186 the \emph{copy Turing program} is left as an excerise to the reader; also |
188 the \emph{copy Turing program} is left as an excerise to the reader; also |
518 case a Turing program takes according to the usual textbook |
520 case a Turing program takes according to the usual textbook |
519 definition \cite{Boolos87} less than @{text n} steps before it |
521 definition \cite{Boolos87} less than @{text n} steps before it |
520 halts, then in our setting the @{term steps}-evaluation does not |
522 halts, then in our setting the @{term steps}-evaluation does not |
521 actually halt, but rather transitions to the @{text 0}-state (the |
523 actually halt, but rather transitions to the @{text 0}-state (the |
522 final state) and remains there performing @{text Nop}-actions until |
524 final state) and remains there performing @{text Nop}-actions until |
523 @{text n} is reached. |
525 @{text n} is reached. This is different from the setup in |
|
526 \cite{AspertiRicciotti12} where an option is returned once a final |
|
527 state is reached. |
524 |
528 |
525 \begin{figure}[t] |
529 \begin{figure}[t] |
526 \begin{center} |
530 \begin{center} |
527 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
531 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
528 \begin{tabular}[t]{@ {}l@ {}} |
532 \begin{tabular}[t]{@ {}l@ {}} |
672 |
676 |
673 \noindent |
677 \noindent |
674 whose three components are given in Figure~\ref{copy}. To the prove |
678 whose three components are given in Figure~\ref{copy}. To the prove |
675 correctness of these Turing machine programs, we introduce the |
679 correctness of these Turing machine programs, we introduce the |
676 notion of total correctness defined in terms of |
680 notion of total correctness defined in terms of |
677 \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the |
681 \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar |
|
682 to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. |
|
683 They implement the |
678 idea that a program @{term p} started in state @{term "1::nat"} with |
684 idea that a program @{term p} started in state @{term "1::nat"} with |
679 a tape satisfying @{term P} will after some @{text n} steps halt (have |
685 a tape satisfying @{term P} will after some @{text n} steps halt (have |
680 transitioned into the halting state) with a tape satisfying @{term |
686 transitioned into the halting state) with a tape satisfying @{term |
681 Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"} |
687 Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"} |
682 realising the case that a program @{term p} started with a tape |
688 realising the case that a program @{term p} started with a tape |
701 \end{tabular} |
707 \end{tabular} |
702 \end{tabular} |
708 \end{tabular} |
703 \end{center} |
709 \end{center} |
704 |
710 |
705 \noindent |
711 \noindent |
706 We have set up our Hoare-style reasoning so that we can deal explicitly |
712 Like Asperti and Ricciotti with their notion of realisability, we |
707 with total correctness and non-terminantion, rather than have notions for partial |
713 have set up our Hoare-style reasoning so that we can deal explicitly |
708 correctness and termination. Although the latter would allow us to reason |
714 with total correctness and non-terminantion, rather than have |
709 more uniformly (only using Hoare-triples), we prefer our definitions because |
715 notions for partial correctness and termination. Although the latter |
710 we can derive simple Hoare-rules for sequentially composed Turing programs. |
716 would allow us to reason more uniformly (only using Hoare-triples), |
711 In this way we can reason about the correctness of @{term "tcopy_init"}, |
717 we prefer our definitions because we can derive (below) simple |
712 for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}. |
718 Hoare-rules for sequentially composed Turing programs. In this way |
|
719 we can reason about the correctness of @{term "tcopy_init"}, for |
|
720 example, completely separately from @{term "tcopy_loop"} and @{term |
|
721 "tcopy_end"}. |
|
722 |
|
723 It is realatively straightforward to prove that the Turing program |
|
724 @{term "dither"} shown in \eqref{dither} is correct. This program |
|
725 should be the ``identity'' when started with a standard tape representing |
|
726 @{text "1"} but loop when started with @{text 0} instead. |
|
727 |
713 |
728 |
714 \begin{center} |
729 \begin{center} |
715 \begin{tabular}{l@ {\hspace{3mm}}lcl} |
730 \begin{tabular}{l@ {\hspace{3mm}}lcl} |
716 & \multicolumn{1}{c}{start tape}\\[1mm] |
731 & \multicolumn{1}{c}{start tape}\\[1mm] |
717 \raisebox{2.5mm}{halting case:} & |
732 \raisebox{2mm}{halting case:} & |
718 \begin{tikzpicture}[scale=0.9] |
733 \begin{tikzpicture}[scale=0.8] |
719 \draw[very thick] (-2,0) -- ( 0.75,0); |
734 \draw[very thick] (-2,0) -- ( 0.75,0); |
720 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
735 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
721 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
736 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
722 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
737 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
723 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
738 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
726 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
741 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
727 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
742 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
728 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
743 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
729 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
744 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
730 \end{tikzpicture} |
745 \end{tikzpicture} |
731 & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} & |
746 & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} & |
732 \begin{tikzpicture}[scale=0.9] |
747 \begin{tikzpicture}[scale=0.8] |
733 \draw[very thick] (-2,0) -- ( 0.75,0); |
748 \draw[very thick] (-2,0) -- ( 0.75,0); |
734 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
749 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
735 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
750 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
736 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
751 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
737 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
752 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
741 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
756 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
742 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
757 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
743 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
758 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
744 \end{tikzpicture}\\ |
759 \end{tikzpicture}\\ |
745 |
760 |
746 \raisebox{2.5mm}{non-halting case:} & |
761 \raisebox{2mm}{non-halting case:} & |
747 \begin{tikzpicture}[scale=0.9] |
762 \begin{tikzpicture}[scale=0.8] |
748 \draw[very thick] (-2,0) -- ( 0.25,0); |
763 \draw[very thick] (-2,0) -- ( 0.25,0); |
749 \draw[very thick] (-2,0.5) -- ( 0.25,0.5); |
764 \draw[very thick] (-2,0.5) -- ( 0.25,0.5); |
750 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
765 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
751 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
766 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
752 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
767 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
753 \draw[very thick] (-1.25,0) -- (-1.25,0.5); |
768 \draw[very thick] (-1.25,0) -- (-1.25,0.5); |
754 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
769 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
755 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
770 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
756 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
771 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
757 \end{tikzpicture} |
772 \end{tikzpicture} |
758 & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} & |
773 & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} & |
759 \raisebox{2.5mm}{loops} |
774 \raisebox{2mm}{loops} |
760 \end{tabular} |
775 \end{tabular} |
761 \end{center} |
776 \end{center} |
762 |
777 |
763 |
778 \noindent |
764 It is straightforward to prove that the Turing program |
779 We can prove the following formal statements |
765 @{term "dither"} satisfies the following correctness properties |
780 |
766 |
|
767 \begin{center} |
781 \begin{center} |
768 \begin{tabular}{l} |
782 \begin{tabular}{l} |
769 @{thm dither_halts}\\ |
783 @{thm dither_halts}\\ |
770 @{thm dither_loops} |
784 @{thm dither_loops} |
771 \end{tabular} |
785 \end{tabular} |