522 \caption{Copy machine}\label{copy} |
521 \caption{Copy machine}\label{copy} |
523 \end{figure} |
522 \end{figure} |
524 |
523 |
525 Before we can prove the undecidability of the halting problem for |
524 Before we can prove the undecidability of the halting problem for |
526 Turing machines, we need to analyse two concrete Turing machine |
525 Turing machines, we need to analyse two concrete Turing machine |
527 programs and establish that they are correct, that is they are |
526 programs and establish that they are correct, that means they are |
528 ``doing what they are supposed to be doing''. This is usually left |
527 ``doing what they are supposed to be doing''. This is usually left |
529 out in the informal literature, for example \cite{Boolos87}. One program |
528 out in the informal literature, for example \cite{Boolos87}. One program |
530 we prove correct is the @{term dither} program shown in \eqref{dither} |
529 we need to prove correct is the @{term dither} program shown in \eqref{dither} |
531 and the other program @{term "tcopy"} is defined as |
530 and the other program @{term "tcopy"} is defined as |
532 |
531 |
533 \begin{center} |
532 \begin{center} |
534 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
533 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
535 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
534 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
536 \end{tabular} |
535 \end{tabular} |
537 \end{center} |
536 \end{center} |
538 |
537 |
539 \noindent |
538 \noindent |
540 whose three components are given in Figure~\ref{copy}. |
539 whose three components are given in Figure~\ref{copy}. To prove correctness, |
541 |
540 we introduce the notion of total correctness defined in terms of |
542 |
541 \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the idea |
543 |
542 that a program @{term p} started in state @{term "1::nat"} with a tape |
544 |
543 satisfying @{term P} will after @{text n} steps halt (have transitioned into |
545 |
544 the halting state) with a tape satisfying @{term Q}. We also have |
546 To prove the correctness, we derive some Hoare-style reasoning rules for |
545 \emph{Hoare-pairs} of the form @{term "{P} p \<up>"} realising the case that a |
547 Turing machine programs. A \emph{Hoare-triple} for a terminating Turing |
546 program @{term p} started with a tape satisfying @{term P} will loop |
548 machine program is defined as |
547 (never transition into the halting state). Both notion are formally |
549 |
548 defined as |
550 \begin{center} |
549 |
551 @{thm Hoare_halt_def} |
550 \begin{center} |
552 \end{center} |
551 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
553 |
552 \begin{tabular}[t]{@ {}l@ {}} |
554 A \emph{Hoare-pair} for a non-terminating Turing machine program is defined |
553 @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\ |
555 as |
554 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
556 |
555 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
557 \begin{center} |
556 \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\ |
558 @{thm Hoare_unhalt_def} |
557 \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
559 \end{center} |
558 \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} |
560 |
559 \end{tabular} & |
561 |
560 \begin{tabular}[t]{@ {}l@ {}} |
|
561 @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\ |
|
562 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
|
563 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
|
564 \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} |
|
565 \end{tabular} |
|
566 \end{tabular} |
|
567 \end{center} |
|
568 |
|
569 \noindent |
|
570 We have set up our Hoare-style reasoning to deal explicitly with |
|
571 looping and total correctness, rather separate notions for partial |
|
572 correctness and termination, is because we can derive simple rules |
|
573 for sequentially composed Turing programs. They allow us to reason |
|
574 about correctness of components completely separately. |
|
575 |
|
576 It is rather straightforward to prove that the Turing program |
|
577 @{term "dither"} satisfies the following correctness properties |
|
578 |
|
579 \begin{center} |
|
580 \begin{tabular}{l} |
|
581 @{thm dither_halts}\\ |
|
582 @{thm dither_loops} |
|
583 \end{tabular} |
|
584 \end{center} |
|
585 |
|
586 \noindet |
|
587 {\it unfold} The first states that on a tape @{term "(Bk \<up> n, [Oc, Oc])"} |
|
588 halts in tree steps leaving the tape unchanged. In the other states |
|
589 that @{term dither} started with tape @{term "(Bk \<up> n, [Oc, Oc])"} loops. |
|
590 |
562 |
591 |
563 |
592 |
564 In the following we will consider the following Turing machine program |
593 In the following we will consider the following Turing machine program |
565 that makes a copies a value on the tape. |
594 that makes a copies a value on the tape. |
566 |
595 |