tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:c3832c4963c4
+:1e89c65f844b
 layout_of ("layout") and
 findnth ("find'_nth") and
 recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
 Pr ("Pr\<^isup>_") and
 Cn ("Cn\<^isup>_") and
-Mn ("Mn\<^isup>_")
+Mn ("Mn\<^isup>_") and
+rec_calc_rel ("eval") and
+tm_of_rec ("translate")
 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
 ``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 by Boolos
 et al \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
+the \emph{copy Turing machine} is left as an exercise to the
 reader---a corresponding correctness proof is not mentioned at all; 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
 the head and @{term r} for the tape on the right-hand side.  We use
 the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
 composed of @{term n} elements of @{term Bk}s.  We also have the
 convention that the head, abbreviated @{term hd}, of the right list
 is the cell on which the head of the Turing machine currently
-scannes. This can be pictured as follows:
+scans. This can be pictured as follows:
 %
 \begin{center}
 \begin{tikzpicture}[scale=0.9]
 \draw[very thick] (-3.0,0)   -- ( 3.0,0);
 \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
 @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
 \end{tabular}
 \end{center}
 \noindent
-The first adds @{text n} to all states, exept the @{text 0}-state,
+The first adds @{text n} to all states, except the @{text 0}-state,
 thus moving all ``regular'' states to the segment starting at @{text
 n}; the second adds @{term "Suc(length p div 2)"} to the @{text
 0}-state, thus redirecting all references to the ``halting state''
 to the first state after the program @{text p}.  With these two
 functions in place, we can define the \emph{sequential composition}
 \end{figure}
 We often need to restrict tapes to be in 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
+the right list contains some ``clusters'' of @{text "Oc"}s separated by single
 blanks. To make this formal we define the following overloaded function
 encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.
 %
 \begin{equation}
 \mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
 @{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}).
 Like Asperti and Ricciotti with their notion of realisability, we
 have set up our Hoare-rules so that we can deal explicitly
-with total correctness and non-terminantion, rather than have
+with total correctness and non-termination, 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 some simple
 Hoare-rules for sequentially composed Turing programs.  In this way
 we can reason about the correctness of @{term "tcopy_begin"}, for
 example, completely separately from @{term "tcopy_loop"} and @{term
 "tcopy_end"}.
-It is realatively straightforward to prove that the Turing program
+It is relatively 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 loops when started with the @{text 0}-representation instead, as pictured
 below.
 We next need to show that @{term "tcopy_begin"} terminates. For this
 we introduce lexicographically ordered pairs @{term "(n, m)"}
 derived from configurations @{text "(s, (l, r))"} whereby @{text n} is
 the state @{text s}, but ordered according to how @{term tcopy_begin} executes
 them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have
-a strictly decreasing meansure, @{term m} takes the data on the tape into
+a strictly decreasing measure, @{term m} takes the data on the tape into
 account and is calculated according to the following measure function:
 \begin{center}
 \begin{tabular}{rcl}
 @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} &
 That means if we start with a tape of the form @{term "([], <n::nat>)"} then
 @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}, as desired.
 Finally, we are in the position to prove the undecidability of the halting problem.
 A program @{term p} started with a standard tape containing the (encoded) numbers
-@{term ns} will \emph{halt} with a standard tape containging a single (encoded)
+@{term ns} will \emph{halt} with a standard tape containing a single (encoded)
 number is defined as
 \begin{center}
 @{thm haltP_def}
 \end{center}
 \end{center}
 \noindent
 This time the Hoare-triple states that @{term tcontra} terminates
 with the ``output'' @{term "<(1::nat)>"}. In both case we come
-to a contradiction, which means we have to abondon our assumption
+to a contradiction, which means we have to abandon our assumption
 that there exists a Turing machine @{term H} which can in general decide
 whether Turing machines terminate.
 *}
 \noindent
 where @{text n} indicates the function expects @{term n} arguments
 (@{text z} and @{term s} expect one argument), and @{text rs} stands
 for a list of recursive functions. Since we know in each case
-the arity, say @{term n}, we can define an inductive relation that
+the arity, say @{term l}, we can define an inductive evaluation relation that
-relates a recursive function and a list of natural numbers of length @{text n},
+relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l},
-to what the result of the recurisve function is---we omit the straightforward
+to what the result of the recursive function is, say @{text n}---we omit the straightforward
-definition. Because of space reasons, we also omit the definition of translating
+definition of @{term "rec_cal_rel r ns n"}. Because of space reasons, we also omit the
-recursive functions into abacus programs and the also the definition of the
+definition of translating
+recursive functions into abacus programs. We can prove the following
+theorem about the translation: Assuming
+@{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
+then the following Hoare-triple holds
+\begin{center}
+@{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
+\end{center}
+\noindent
+which means that if the recursive function @{text r} with arguments @{text ns} evaluates
+to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started
+with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
+with the standard tape @{term "(Bk \<up> l, <n::nat> @ Bk \<up> m)"} for some @{text l} and @{text m}.
+and the also the definition of the
 universal function (we refer the reader to our formalisation).
 *}
 (*
 precisely as Boolos et al present it, but use definitions that make
 mechanised proofs manageable. For example our definition of the
 halting state performing @{term Nop}-operations seems to be non-standard,
 but very much suited to a formalisation in a theorem prover where
 the @{term steps}-function need to be total. We have found an
-inconsitency in
+inconsistency in
 Bolos et al's usage of definitions of \ldots
 Our interest in Turing machines
 arose from correctness proofs about algorithms where we were unable
 to formalise arguments about decidability but also undecidability
 proofs in general (for example Wang's tiling problem \cite{Robinson71}).
 undecidability of the halting problem for Turing machines.  This
 took us around 1500 loc of Isar-proofs, which is just one-and-a-half
 times longer than a mechanised proof pearl about the Myhill-Nerode
 theorem. So our conclusion is it not as daunting as we imagined
 reading the paper by Norrish \cite{Norrish11}. The work involved
-with constructing a universial Turing machine via recursive
+with constructing a universal Turing machine via recursive
 functions and abacus machines, on the other hand, is not a
 project one wants to undertake too many times (our formalisation
 of abacus machines and their correct translation is approximately
 4300 loc; \ldots)
 machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the
 Matita theorem prover. It turns out that their notion of
 realisability and our Hoare-triples are very similar, however we
 differ in some basic definitions for Turing machines. Asperti and
 Ricciotti are interested in providing a mechanised foundation for
-complexity theory. They formalised a universial Turing machine
+complexity theory. They formalised a universal Turing machine
 (which differs from ours by using a more general alphabet), but did
 not describe an undecidability proof. Given their definitions and
 infrastructure, we expect this should not be too difficult for them.
 For us the most interesting aspect of our work are the correctness
 proofs for some Turing machines. Informal presentation of computability
 theory often leave the constructions of particular Turing machines
-as excercise to the reader, as \cite{Boolos87} for example, deeming it
+as exercise to the reader, as \cite{Boolos87} for example, deeming it
 too easy for wasting space. However, as far as we are aware all
 informal presentation leave out any correctness proofs---do the
 Turing machines really perform the task they are supposed to do.
 This means we have to find appropriate invariants and measures
-that can be establised for showing correctness and termination.
+that can be established for showing correctness and termination.
 Whenever we can use Hoare-style reasoning, the invariants are
 relatively straightforward and much smaller than for example
 the invariants by Myreen for a correctness proof of a garbage
 collector \cite[Page 76]{}. The invariant needed for the abacus proof,
 where Hoare-style reasoning does not work, is similar in size as
 the one by Myreen and finding a sufficiently strong one took
-us, like Myreen, something on the magnitute of weeks.
+us, like Myreen, something on the magnitude of weeks.
 Our reasoning about the invariants is also not very much
 supported by the automation in Isabelle. There is however a tantalising
 connection between our work and recent work \cite{Jensen13}
 on verifying X86 assembly code. They observed a similar phenomenon
-with assmebly programs that Hoare-style reasoning is sometimes
+with assembly programs that Hoare-style reasoning is sometimes
 possible, but sometimes not. In order to ease their reasoning they
 introduced a more primitive specification logic, on which
 for special cases Hoare-rules can be provided.
 It remains to be seen whether their specification logic
-for assmebly code can make it easier to reason about our Turing
+for assembly code can make it easier to reason about our Turing
 programs. That would be an attractive result, because Turing
 machine programs are
 The code of our formalisation is available from the Mercurial repository at
 \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}

changeset 130	1e89c65f844b
parent 129	c3832c4963c4
child 132	264ff7014657