131 \noindent |
131 \noindent |
132 In this paper we take on this daunting prospect and provide a |
132 In this paper we take on this daunting prospect and provide a |
133 formalisation of Turing machines, as well as abacus machines (a kind |
133 formalisation of Turing machines, as well as abacus machines (a kind |
134 of register machines) and recursive functions. To see the difficulties |
134 of register machines) and recursive functions. To see the difficulties |
135 involved with this work, one has to understand that Turing machine |
135 involved with this work, one has to understand that Turing machine |
136 programs can be completely \emph{unstructured}, behaving |
136 programs can be completely \emph{unstructured}, behaving similar to |
137 similar to Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the |
137 Basic programs involving the infamous goto \cite{Dijkstra68}. This |
138 general case a compositional Hoare-style reasoning about Turing |
138 precludes in the general case a compositional Hoare-style reasoning |
139 programs. We provide such Hoare-rules for when it \emph{is} possible to |
139 about Turing programs. We provide such Hoare-rules for when it |
140 reason in a compositional manner (which is fortunately quite often), but also tackle |
140 \emph{is} possible to reason in a compositional manner (which is |
141 the more complicated case when we translate abacus programs into |
141 fortunately quite often), but also tackle the more complicated case |
142 Turing programs. This reasoning about Turing machine programs is |
142 when we translate abacus programs into Turing programs. This |
143 usually completely left out in the informal literature, e.g.~\cite{Boolos87}. |
143 reasoning about concrete Turing machine programs is usually |
|
144 left out in the informal literature, e.g.~\cite{Boolos87}. |
144 |
145 |
145 %To see the difficulties |
146 %To see the difficulties |
146 %involved with this work, one has to understand that interactive |
147 %involved with this work, one has to understand that interactive |
147 %theorem provers, like Isabelle/HOL, are at their best when the |
148 %theorem provers, like Isabelle/HOL, are at their best when the |
148 %data-structures at hand are ``structurally'' defined, like lists, |
149 %data-structures at hand are ``structurally'' defined, like lists, |
228 translating recursive functions to abacus machines and abacus machines to |
229 translating recursive functions to abacus machines and abacus machines to |
229 Turing machines. Since we have set up in Isabelle/HOL a very general computability |
230 Turing machines. Since we have set up in Isabelle/HOL a very general computability |
230 model and undecidability result, we are able to formalise other |
231 model and undecidability result, we are able to formalise other |
231 results: we describe a proof of the computational equivalence |
232 results: we describe a proof of the computational equivalence |
232 of single-sided Turing machines, which is not given in \cite{Boolos87}, |
233 of single-sided Turing machines, which is not given in \cite{Boolos87}, |
233 but needed for formalising the undecidability proof of Wang's tiling problem. {\it citation} |
234 but needed for example for formalising the undecidability proof of |
|
235 Wang's tiling problem \cite{Robinson71}. |
234 %We are not aware of any other |
236 %We are not aware of any other |
235 %formalisation of a substantial undecidability problem. |
237 %formalisation of a substantial undecidability problem. |
236 *} |
238 *} |
237 |
239 |
238 section {* Turing Machines *} |
240 section {* Turing Machines *} |
264 \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); |
266 \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); |
265 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
267 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
266 \draw[fill] (1.35,0.1) rectangle (1.65,0.4); |
268 \draw[fill] (1.35,0.1) rectangle (1.65,0.4); |
267 \draw[fill] (0.85,0.1) rectangle (1.15,0.4); |
269 \draw[fill] (0.85,0.1) rectangle (1.15,0.4); |
268 \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); |
270 \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); |
|
271 \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4); |
269 \draw (-0.25,0.8) -- (-0.25,-0.8); |
272 \draw (-0.25,0.8) -- (-0.25,-0.8); |
270 \draw[<->] (-1.25,-0.7) -- (0.75,-0.7); |
273 \draw[<->] (-1.25,-0.7) -- (0.75,-0.7); |
271 \node [anchor=base] at (-0.8,-0.5) {\small left list}; |
274 \node [anchor=base] at (-0.8,-0.5) {\small left list}; |
272 \node [anchor=base] at (0.35,-0.5) {\small right list}; |
275 \node [anchor=base] at (0.35,-0.5) {\small right list}; |
273 \node [anchor=base] at (0.1,0.7) {\small head}; |
276 \node [anchor=base] at (0.1,0.7) {\small head}; |
520 \end{tabular} |
523 \end{tabular} |
521 \end{center} |
524 \end{center} |
522 \caption{Copy machine}\label{copy} |
525 \caption{Copy machine}\label{copy} |
523 \end{figure} |
526 \end{figure} |
524 |
527 |
525 {\it tapes in standard form} |
528 {\it |
|
529 As in \cite{Boolos87} we often need to restrict tapes to be in standard |
|
530 form.} |
526 |
531 |
527 Before we can prove the undecidability of the halting problem for our |
532 Before we can prove the undecidability of the halting problem for our |
528 Turing machines, we need to analyse two concrete Turing machine |
533 Turing machines, we need to analyse two concrete Turing machine |
529 programs and establish that they are correct---that means they are |
534 programs and establish that they are correct---that means they are |
530 ``doing what they are supposed to be doing''. Such correctness proofs are usually left |
535 ``doing what they are supposed to be doing''. Such correctness proofs are usually left |
531 out in the informal literature, for example \cite{Boolos87}. One program |
536 out in the informal literature, for example \cite{Boolos87}. One program |
532 we need to prove correct is the @{term dither} program shown in \eqref{dither} |
537 we need to prove correct is the @{term dither} program shown in \eqref{dither} |
533 and the other program is @{term "tcopy"} is defined as |
538 and the other program is @{term "tcopy"} defined as |
534 |
539 |
535 \begin{center} |
540 \begin{center} |
536 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
541 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
537 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
542 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
538 \end{tabular} |
543 \end{tabular} |
552 state). Both notion are formally defined as |
557 state). Both notion are formally defined as |
553 |
558 |
554 \begin{center} |
559 \begin{center} |
555 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
560 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
556 \begin{tabular}[t]{@ {}l@ {}} |
561 \begin{tabular}[t]{@ {}l@ {}} |
557 @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\[1mm] |
562 \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm] |
558 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
563 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
559 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
564 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
560 \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\ |
565 \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\ |
561 \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
566 \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
562 \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} |
567 \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} |
563 \end{tabular} & |
568 \end{tabular} & |
564 \begin{tabular}[t]{@ {}l@ {}} |
569 \begin{tabular}[t]{@ {}l@ {}} |
565 @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\[1mm] |
570 \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm] |
566 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
571 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
567 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
572 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
568 \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} |
573 \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} |
569 \end{tabular} |
574 \end{tabular} |
570 \end{tabular} |
575 \end{tabular} |
575 with looping and total correctness, rather than have notions for partial |
580 with looping and total correctness, rather than have notions for partial |
576 correctness and termination. Although the latter would allow us to reason |
581 correctness and termination. Although the latter would allow us to reason |
577 more uniformly (only using Hoare-triples), we prefer our definitions because |
582 more uniformly (only using Hoare-triples), we prefer our definitions because |
578 we can derive simple Hoare-rules for sequentially composed Turing programs. |
583 we can derive simple Hoare-rules for sequentially composed Turing programs. |
579 In this way we can reason about the correctness of @{term "tcopy_init"}, |
584 In this way we can reason about the correctness of @{term "tcopy_init"}, |
580 for example, completely separately from @{term "tcopy_loop"}. |
585 for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}. |
581 |
586 |
582 It is rather straightforward to prove that the Turing program |
587 \begin{center} |
|
588 \begin{tabular}{lcl} |
|
589 \multicolumn{1}{c}{start tape}\\ |
|
590 \begin{tikzpicture} |
|
591 \draw[very thick] (-2,0) -- ( 0.75,0); |
|
592 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
|
593 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
|
594 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
|
595 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
|
596 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
|
597 \draw[very thick] (-1.25,0) -- (-1.25,0.5); |
|
598 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
|
599 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
|
600 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
|
601 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
|
602 \end{tikzpicture} |
|
603 & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} & |
|
604 \begin{tikzpicture} |
|
605 \draw[very thick] (-2,0) -- ( 0.75,0); |
|
606 \draw[very thick] (-2,0.5) -- ( 0.75,0.5); |
|
607 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
|
608 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
|
609 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
|
610 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
|
611 \draw[very thick] (-1.25,0) -- (-1.25,0.5); |
|
612 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
|
613 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
|
614 \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); |
|
615 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
|
616 \end{tikzpicture}\\ |
|
617 |
|
618 \begin{tikzpicture} |
|
619 \draw[very thick] (-2,0) -- ( 0.25,0); |
|
620 \draw[very thick] (-2,0.5) -- ( 0.25,0.5); |
|
621 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
|
622 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
|
623 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
|
624 \draw[very thick] (-1.25,0) -- (-1.25,0.5); |
|
625 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
|
626 \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); |
|
627 \node [anchor=base] at (-1.7,0.2) {\ldots}; |
|
628 \end{tikzpicture} |
|
629 & \raisebox{2.5mm}{$\;\;\large\Rightarrow\;\;$} & |
|
630 \raisebox{2.5mm}{loops} |
|
631 \end{tabular} |
|
632 \end{center} |
|
633 |
|
634 |
|
635 It is straightforward to prove that the Turing program |
583 @{term "dither"} satisfies the following correctness properties |
636 @{term "dither"} satisfies the following correctness properties |
584 |
637 |
585 \begin{center} |
638 \begin{center} |
586 \begin{tabular}{l} |
639 \begin{tabular}{l} |
587 @{thm dither_halts}\\ |
640 @{thm dither_halts}\\ |