--- a/Paper/Paper.thy Wed Feb 06 03:37:26 2013 +0000
+++ b/Paper/Paper.thy Wed Feb 06 04:11:06 2013 +0000
@@ -89,7 +89,9 @@
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:
@@ -270,7 +272,7 @@
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
@@ -349,7 +351,7 @@
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]
@@ -549,7 +551,7 @@
\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''
@@ -728,7 +730,7 @@
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.
%
@@ -812,7 +814,7 @@
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
@@ -821,7 +823,7 @@
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
@@ -986,7 +988,7 @@
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}
@@ -1033,7 +1035,7 @@
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}
@@ -1133,7 +1135,7 @@
\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.
*}
@@ -1302,11 +1304,27 @@
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
- relates a recursive function and a list of natural numbers of length @{text n},
- to what the result of the recurisve function is---we omit the straightforward
- definition. Because of space reasons, we also omit the definition of translating
- recursive functions into abacus programs and the also the definition of the
+ the arity, say @{term l}, we can define an inductive evaluation relation that
+ relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l},
+ to what the result of the recursive function is, say @{text n}---we omit the straightforward
+ definition of @{term "rec_cal_rel r ns n"}. Because of space reasons, we also omit 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).
*}
@@ -1332,7 +1350,7 @@
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
@@ -1354,7 +1372,7 @@
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
@@ -1366,7 +1384,7 @@
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.
@@ -1374,30 +1392,30 @@
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