--- a/Paper/Paper.thy Tue Jan 29 16:37:38 2013 +0000
+++ b/Paper/Paper.thy Wed Jan 30 02:26:56 2013 +0000
@@ -35,7 +35,41 @@
tcopy ("copy") and
tape_of ("\<langle>_\<rangle>") and
tm_comp ("_ \<oplus> _") and
- DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>")
+ DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") and
+ inv_begin0 ("I\<^isub>0") and
+ inv_begin1 ("I\<^isub>1") and
+ inv_begin2 ("I\<^isub>2") and
+ inv_begin3 ("I\<^isub>3") and
+ inv_begin4 ("I\<^isub>4") and
+ inv_begin ("I\<^bsub>begin\<^esub>")
+
+
+lemma inv_begin_print:
+ shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
+ "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and
+ "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and
+ "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and
+ "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
+ "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
+apply(case_tac [!] tp)
+by (auto)
+
+lemma inv1:
+ shows "0 < n \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"
+unfolding assert_imp_def
+unfolding inv_loop1.simps inv_begin0.simps
+apply(auto)
+apply(rule_tac x="1" in exI)
+apply(auto simp add: replicate.simps)
+done
+
+lemma inv2:
+ shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
+apply(rule ext)
+apply(case_tac x)
+apply(simp add: inv_end1.simps)
+done
+
declare [[show_question_marks = false]]
@@ -73,12 +107,15 @@
lemma nats2tape:
shows "<([]::nat list)> = []"
- and "<[n]> = Oc \<up> (n + 1)"
- and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
-apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
+ and "<[n]> = <n>"
+ and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"
+ and "<(n, m)> = <n> @ [Bk] @ <m>"
+ and "<[n, m]> = <(n, m)>"
+ and "<n> = Oc \<up> (n + 1)"
+apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)
apply(case_tac ns)
-apply(auto)
-done
+apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)
+done
lemmas HR1 =
Hoare_plus_halt_simple[where ?P1.0="P" and ?P2.0="Q" and ?P3.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
@@ -86,6 +123,16 @@
lemmas HR2 =
Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+lemma inv_begin01:
+ assumes "n > 1"
+ shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
+using assms by auto
+
+lemma inv_begin02:
+ assumes "n = 1"
+ shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
+using assms by auto
+
(*>*)
section {* Introduction *}
@@ -179,26 +226,27 @@
%standard proof of this property uses the notion of universal
%Turing machines.
-We are not the first who formalised Turing machines: we are aware
-of the 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. 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
+We are not the first who formalised Turing machines: we are aware of
+the 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. 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
detailed. Some details are left out however: for example, constructing
-the \emph{copy Turing machine} is left as an excerise to the reader; also
-\cite{Boolos87} only shows how the universal Turing machine is constructed for Turing
-machines computing unary functions. We had to figure out a way to
-generalise this result to $n$-ary functions. Similarly, when compiling
-recursive functions to abacus machines, the textbook again only shows
-how it can be done for 2- and 3-ary functions, but in the
-formalisation we need arbitrary functions. But the general ideas for
-how to do this are clear enough in \cite{Boolos87}.
+the \emph{copy Turing machine} and its correctness proof are left as
+an excerise to the reader; also \cite{Boolos87} only shows how the
+universal Turing machine is constructed for Turing machines computing
+unary functions. We had to figure out a way to generalise this result
+to $n$-ary functions. Similarly, when compiling recursive functions to
+abacus machines, the textbook again only shows how it can be done for
+2- and 3-ary functions, but in the formalisation we need arbitrary
+functions. But the general ideas for how to do this are clear enough
+in \cite{Boolos87}.
%However, one
%aspect that is completely left out from the informal description in
%\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing
@@ -443,7 +491,7 @@
In this definition the function @{term nth_of} returns the @{text n}th element
from a list, provided it exists (@{term Some}-case), or if it does not, it
returns the default action @{term Nop} and the default state @{text 0}
- (@{term None}-case). We often need to restrict Turing machine programs
+ (@{term None}-case). We often have to restrict Turing machine programs
to be well-formed: a program @{term p} is \emph{well-formed} if it
satisfies the following three properties:
@@ -638,10 +686,10 @@
\end{tikzpicture}\\[-8mm]\mbox{}
\end{center}
\caption{The three components of the \emph{copy Turing machine} (above). If started
- (below) with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at
+ (below) with the tape @{term "([], <(2::nat)>)"} the first machine appends @{term "[Bk, Oc]"} at
the end of the right tape; the second then ``moves'' all @{term Oc}s except the
first from the beginning of the tape to the end; the third ``refills'' the original
- block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}
+ block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.}
\label{copy}
\end{figure}
@@ -649,10 +697,14 @@
We often need to restrict tapes to be in \emph{standard form}, which means
the left list of the tape is either empty or only contains @{text "Bk"}s, and
the right list contains some ``clusters'' of @{text "Oc"}s separted by single
- blanks. To make this formal we define the following function
+ blanks. To make this formal we define the following overloaded function
\begin{center}
- \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
+ @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
+ \end{tabular}\hspace{6mm}
+ \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
@{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
@{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
@@ -666,10 +718,10 @@
is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
Before we can prove the undecidability of the halting problem for our
- Turing machines, we need to analyse two concrete Turing machine
+ Turing machines, we have to analyse two concrete Turing machine
programs and establish that they are correct---that means they are
``doing what they are supposed to be doing''. Such correctness proofs are usually left
- out in the informal literature, for example \cite{Boolos87}. One program
+ out in the informal literature, for example \cite{Boolos87}. The first program
we need to prove correct is the @{term dither} program shown in \eqref{dither}
and the other program is @{term "tcopy"} defined as
@@ -680,19 +732,18 @@
\end{equation}
\noindent
- whose three components are given in Figure~\ref{copy}. To the prove
- the correctness of Turing machine programs, we introduce the
- notion of total correctness defined in terms of
- \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
- Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
- implementing the case that a program @{term p} started with a tape
- satisfying @{term P} will loop (never transition into the halting
- state). Both notion are formally defined as
+ whose three components are given in Figure~\ref{copy}. We introduce
+ the notion of total correctness defined in terms of
+ \emph{Hoare-triples}, written @{term "{P} p {Q}"} (this notion is
+ very similar to \emph{realisability} in \cite{AspertiRicciotti12}).
+ The Hoare-triples 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 Q}. We also have
+ \emph{Hoare-pairs} of the form @{term "{P} p \<up>"} implementing the
+ case that a program @{term p} started with a tape satisfying @{term
+ P} will loop (never transition into the halting state). Both notion
+ are formally defined as
\begin{center}
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
@@ -796,11 +847,11 @@
number of steps we can perform starting from the input tape.
The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
- its purpose is to produce the standard tape @{term "(DUMMY, <[n,
- n::nat]>)"} when started with @{term "(DUMMY, <[n::nat]>)"}, that is
+ its purpose is to produce the standard tape @{term "(DUMMY, <(n,
+ n::nat)>)"} when started with @{term "(DUMMY, <(n::nat)>)"}, that is
making a copy of a value on the tape. Reasoning about this program
is substantially harder than about @{term dither}. To ease the
- burden, we prove the following two Hoare-rules for sequentially
+ burden, we derive the following two Hoare-rules for sequentially
composed programs.
\begin{center}
@@ -825,23 +876,56 @@
in order to ensure that the redirection of the halting and initial
state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
+ The Hoare-rules above allow us to prove the correctness of @{term tcopy}
+ by considering the correctness of the components @{term "tcopy_begin"}, @{term "tcopy_loop"}
+ and @{term "tcopy_end"} in isolation. We will show the details for
+ the program @{term "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, @{term "inv_begin4"}
+ shown in Figure~\ref{invbegin},
+ we define the following invariant for @{term "tcopy_begin"}.
- The Hoare-rules above allow us to prove the correctness of @{term tcopy}
- by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"}
- and @{term "tcopy_end"} in isolation. We will show the details for
- the program @{term "tcopy_begin"}. We found the following invariants for each
- state:
+ \begin{figure}
+ \begin{center}
+ \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
+ @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
+ & & @{thm (rhs) inv_begin02} \\
+ @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
+ @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
+ @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
+ @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}
+ \end{tabular}
+ \end{center}
+ \caption{The invariants for each state of @{term tcopy_begin}. They depend on
+ the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin}
+ \end{figure}
\begin{center}
- @{thm inv_begin0.simps}\\
- @{thm inv_begin1.simps}\\
- @{thm inv_begin2.simps}\\
- @{thm inv_begin3.simps}\\
- @{thm inv_begin4.simps}
+ \begin{tabular}{rcl}
+ @{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} &
+ @{text "if"} @{thm (prem 1) inv_begin_print(1)} @{text then} @{thm (rhs) inv_begin_print(1)}\\
+ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(2)} @{text then} @{thm (rhs) inv_begin_print(2)} \\
+ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(3)} @{text then} @{thm (rhs) inv_begin_print(3)}\\
+ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(4)} @{text then} @{thm (rhs) inv_begin_print(4)}\\
+ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(5)} @{text then} @{thm (rhs) inv_begin_print(5)}\\
+ & & @{text else} @{thm (rhs) inv_begin_print(6)}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ This definition depends on @{term n}, which represents the number
+ of @{term Oc}s on the tape. It is not hard (26 lines of automated proof script)
+ to show that for @{term "n > (0::nat)"} this invariant is preserved under @{term step} and @{term steps}.
+
+
+ measure for the copying TM, which we however omit.
+
+
+ \begin{center}
+ @{thm begin_correct}\\
+ @{thm loop_correct}\\
+ @{thm end_correct}
\end{center}
- measure for the copying TM, which we however omit.
\begin{center}
@{thm haltP_def[where lm="ns"]}