--- a/Paper/Paper.thy Tue Feb 05 12:41:00 2013 +0000
+++ b/Paper/Paper.thy Wed Feb 06 02:25:00 2013 +0000
@@ -1,11 +1,11 @@
(*<*)
theory Paper
-imports "../thys/abacus"
+imports "../thys/recursive"
begin
-(*
+
hide_const (open) s
-*)
+
hide_const (open) Divides.adjust
@@ -85,7 +85,11 @@
inv_end0 ("K\<^isub>0") and
measure_begin_step ("M\<^bsub>cbegin\<^esub>") and
layout_of ("layout") and
- findnth ("find'_nth")
+ 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>_")
lemma inv_begin_print:
@@ -155,9 +159,9 @@
lemma layout:
shows "layout_of [] = []"
- and "layout_of ((Inc R\<iota>)#os) = (2 * R\<iota> + 9)#(layout_of os)"
- and "layout_of ((Dec R\<iota> i)#os) = (2 * R\<iota> + 16)#(layout_of os)"
- and "layout_of ((Goto i)#os) = 1#(layout_of os)"
+ and "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)"
+ and "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)"
+ and "layout_of ((Goto l)#is) = 1#(layout_of is)"
by(auto simp add: layout_of.simps length_of.simps)
@@ -223,7 +227,7 @@
of register machines) and recursive functions. To see the difficulties
involved with this work, one has to understand that Turing machine
programs can be completely \emph{unstructured}, behaving similar to
-Basic programs containing the infamous goto-statements \cite{Dijkstra68}. This
+Basic programs containing the infamous gotos \cite{Dijkstra68}. This
precludes in the general case a compositional Hoare-style reasoning
about Turing programs. We provide such Hoare-rules for when it
\emph{is} possible to reason in a compositional manner (which is
@@ -267,7 +271,7 @@
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
-reader---a correctness proof is not mentioned at all; also \cite{Boolos87}
+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
@@ -484,7 +488,7 @@
%
\noindent
the reader can see we have organised our Turing machine programs so
- that segments of two belong to a state. The first component of such a
+ that segments of two pairs belong to a state. The first component of such a
segment determines what action should be taken and which next state
should be transitioned to in case the head reads a @{term Bk};
similarly the second component determines what should be done in
@@ -727,9 +731,9 @@
the right list contains some ``clusters'' of @{text "Oc"}s separted 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{center}
- \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ %
+ \begin{equation}
+ \mbox{\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}
@@ -737,12 +741,12 @@
@{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)}
- \end{tabular}
- \end{center}
-
+ \end{tabular}}\label{standard}
+ \end{equation}
+ %
\noindent
A \emph{standard tape} is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l}
- and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
+ and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the
leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
@@ -820,7 +824,7 @@
It is realatively 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 @{text 0} instead, as pictured
+ @{text "1"} but loops when started with the @{text 0}-representation instead, as pictured
below.
@@ -890,7 +894,7 @@
The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
its purpose is to produce the standard tape @{term "(Bks, <(n,
n::nat)>)"} when started with @{term "(Bks, <(n::nat)>)"}, that is
- making a copy of a value on the tape. Reasoning about this program
+ making a copy of a value @{term n} on the tape. Reasoning about this program
is substantially harder than about @{term dither}. To ease the
burden, we derive the following two Hoare-rules for sequentially
composed programs.
@@ -971,7 +975,7 @@
\noindent
This invariant depends on @{term n} representing the number of
- @{term Oc}s (or encoded number) on the tape. It is not hard (26
+ @{term Oc}s@{text "+1"} (or encoded number) 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 the computation rules
@{term step} and @{term steps}. This gives us partial correctness
@@ -979,7 +983,7 @@
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))"}: @{text n} is
+ 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
@@ -1001,7 +1005,7 @@
form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing
machine @{term "tcopy_begin"} will eventually halt (the measure
decreases in each step). Taking this and the partial correctness
- proof together, we obtain the left-most Hoare-triple for @{term tcopy_begin}:
+ proof together, we obtain the Hoare-triple shown on the left for @{term tcopy_begin}:
\begin{center}
@@ -1011,7 +1015,7 @@
\end{center}
\noindent
- where we assume @{text "0 < n"} (similar resoning is needed for
+ where we assume @{text "0 < n"} (similar reasoning is needed for
the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
the halting state of @{term tcopy_begin} implies the invariant of
the starting state of @{term tcopy_loop}, that is @{term "inv_begin0
@@ -1042,7 +1046,7 @@
single number as output. For undecidability, the property we are
proving is that there is no Turing machine that can decide in
general whether a Turing machine program halts (answer either @{text
- 0} for halting and @{text 1} for looping). Given our correctness
+ 0} for halting or @{text 1} for looping). Given our correctness
proofs for @{term dither} and @{term tcopy} shown above, this
non-existence is now relatively straightforward to establish. We first
assume there is a coding function, written @{term "code M"}, which
@@ -1050,7 +1054,7 @@
further assumptions are made about this coding function. Suppose a
Turing machine @{term H} exists such that if started with the
standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0},
- respectively @{text 1}, depending on whether @{text M} halts when
+ respectively @{text 1}, depending on whether @{text M} halts or not when
started with the input tape containing @{term "<ns>"}. This
assumption is formalised as follows---for all @{term M} and all lists of
natural numbers @{term ns}:
@@ -1073,7 +1077,8 @@
\end{center}
\noindent
- Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants on the
+ Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^isub>1"}\ldots@{text "P\<^isub>3"}
+ shown on the
left, we can derive the following Hoare-pair for @{term tcontra} on the right.
\begin{center}\small
@@ -1100,7 +1105,9 @@
This Hoare-pair contradicts our assumption that @{term tcontra} started
with @{term "<(code tcontra)>"} halts.
- Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again given the invariants on the
+ Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again, given the invariants
+ @{text "Q\<^isub>1"}\ldots@{text "Q\<^isub>3"}
+ shown on the
left, we can derive the Hoare-triple for @{term tcontra} on the right.
\begin{center}\small
@@ -1126,7 +1133,7 @@
\noindent
This time the Hoare-triple states that @{term tcontra} terminates
with the ``output'' @{term "<(1::nat)>"}. In both case we come
- to an contradiction, which means we have to abondon our assumption
+ to a contradiction, which means we have to abondon our assumption
that there exists a Turing machine @{term H} which can in general decide
whether Turing machines terminate.
*}
@@ -1138,33 +1145,34 @@
\noindent
Boolos et al \cite{Boolos87} use abacus machines as a stepping stone
for making it less laborious to write Turing machine
- programs. Abacus machines operate over a set of registers $R_0$,
- $R_1$, \ldots{} each being able to hold an arbitrary large natural
+ programs. Abacus machines operate over a set of registers @{text "R\<^isub>0"},
+ @{text "R\<^isub>1"}, \ldots{}, @{text "R\<^isub>n"} each being able to hold an arbitrary large natural
number. We use natural numbers to refer to registers; we also use a natural number
- to represent a program counter and to represent jumping ``addresses''. An abacus
+ to represent a program counter and to represent jumping ``addresses'', for which we
+ use the letter @{text l}. An abacus
program is a list of \emph{instructions} defined by the datatype:
\begin{center}
\begin{tabular}{rcl@ {\hspace{10mm}}l}
@{text "i"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\
- & $\mid$ & @{term "Dec R\<iota> i"} & if content of $R$ is non-zero, then decrement it by one\\
- & & & otherwise jump to instruction $i$\\
- & $\mid$ & @{term "Goto i"} & jump to instruction $i$
+ & $\mid$ & @{term "Dec R\<iota> l"} & if content of $R$ is non-zero, then decrement it by one\\
+ & & & otherwise jump to instruction $l$\\
+ & $\mid$ & @{term "Goto l"} & jump to instruction $l$
\end{tabular}
\end{center}
\noindent
- For example the program clearing the register $R$ (that is setting
+ For example the program clearing the register @{text R} (that is setting
it to @{term "(0::nat)"}) can be defined as follows:
\begin{center}
- @{thm clear.simps[where n="R\<iota>" and e="i", THEN eq_reflection]}
+ @{thm clear.simps[where n="R\<iota>" and e="l", THEN eq_reflection]}
\end{center}
\noindent
Running such a program means we start with the first instruction
then execute one instructions after the other, unless there is a jump. For
- example the second instruction @{term "Goto 0"} in @{term clear} means
+ example the second instruction @{term "Goto 0"} means
we jump back to the first instruction thereby closing the loop. Like with our
Turing machines, we fetch instructions from an abacus program such
that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
@@ -1174,12 +1182,12 @@
all registers.
By convention
the value calculated by an abacus program is stored in the
- last register (the register with the highest index).
+ last register (the one with the highest index in the program).
The main point of abacus programs is to be able to translate them to
Turing machine programs. Registers and their content are represented by
- standard tapes. Because of the jumps in abacus programs, it
- seems difficult to build a Turing machine programs out of components
+ standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it
+ is impossible to build a Turing machine programs out of components
using our @{text "\<oplus>"}-operation shown in the previous section.
To overcome this difficulty, we calculate a \emph{layout} of an
abacus program as follows
@@ -1195,20 +1203,24 @@
\noindent
This gives us a list of natural numbers specifying how many states
- are needed to translate each abacus instruction. The @{text Goto}
- instruction is easiest to translate requiring only one state in
- the corresponding Turing machine:
+ are needed to translate each abacus instruction. This information
+ is needed in order to calculate the state where the Turing program
+ code of one abacus instruction ends.
+ The @{text Goto}
+ instruction is easiest to translate requiring only one state, namely
+ the Turing machine program:
\begin{center}
- @{thm (rhs) tgoto.simps[where n="i"]}
+ @{text "tm_of_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]}
\end{center}
\noindent
- where @{term "i"} is the state in the Turing machine program
- to jump to. For translating the instruction @{term Inc},
+ where @{term "l"} is the state in the Turing machine program
+ to jump to. For translating the instruction @{term "Inc R\<iota>"},
one has to remember that the content of the registers are encoded
- in the Turing machine as standard tape. Therefore the translated Turing machine
- needs to first find the number corresponding to the register @{text "R"}. This needs a machine
+ in the Turing machine as a standard tape. Therefore the translated Turing machine
+ needs to first find the number corresponding to the content of register
+ @{text "R"}. This needs a machine
with @{term "(2::nat) * R\<iota>"} states and can be constructed as follows:
\begin{center}
@@ -1222,11 +1234,11 @@
\noindent
Then we need to increase the ``number'' on the tape by one,
and adjust the following ``registers''. By adjusting we only need to
- replace the first @{term Oc} of each number by @{term Bk} and the last
+ change the first @{term Oc} of each number to @{term Bk} and the last
one from @{term Bk} to @{term Oc}.
Finally, we need to transition the head of the
Turing machine back into the standard position. This requires a Turing machine
- with 9 states (we omit the details). Similarly for the translation of @{term Dec}, where the
+ with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the
translated Turing machine needs to first check whether the content of the
corresponding register is @{text 0}. For this we have a Turing machine program
with @{text 16} states (again details are omitted).
@@ -1236,15 +1248,17 @@
Turing machine component transitions to next one, just like in
the abacus programs. One last problem to overcome is that an abacus
program is assumed to calculate a value stored in the last
- register. That means we have to append a Turing machine that
+ register (the one with the highest register). That means we have to append a Turing machine that
``mops up'' the tape (cleaning all @{text Oc}s) except for the
- @{term Oc}s of the last number represented on the tape.
+ @{term Oc}s of the last number represented on the tape. This needs
+ a Turing machine program with @{text "2 * R + 12"} states, assuming @{text R}
+ is the number of registers to be ``cleaned''.
While generating the Turing machine program for an abacus program is
not too difficult to formalise, the problem is that it contains
@{text Goto}s all over the place. The unfortunate result is that we
cannot use our Hoare-rules for reasoning about sequentially composed
- programs (for this the programs need to be independent). Instead we
+ programs (for this each component needs to be completely independent). Instead we
have to treat the translated Turing machine as one ``big block'' and
prove as invariant that it performs
the same operations as the abacus program. For this we have to show
@@ -1261,7 +1275,40 @@
section {* Recursive Functions and a Universal Turing Machine *}
text {*
+ The main point of recursive functions is that we can relatively
+ easily construct a universal Turing machine via a universal
+ function. This is different from Norrish \cite{Norrish11} who gives a universal
+ function for Church numbers, and also from Asperti and Ricciotti
+ \cite{AspertiRicciotti12} who construct a universal Turing machine
+ directly, but for simulating Turing machines with a more restricted alphabet.
+ \emph{Recursive functions} @{term r} are defined as the datatype
+ \begin{center}
+ \begin{tabular}{c@ {\hspace{4mm}}c}
+ \begin{tabular}{rcl@ {\hspace{4mm}}l}
+ @{term r} & @{text "::="} & @{term z} & (zero-functions)\\
+ & @{text "|"} & @{term s} & (successor-function)\\
+ & @{text "|"} & @{term "id n m"} & (projection)\\
+ \end{tabular} &
+ \begin{tabular}{cl@ {\hspace{4mm}}l}
+ @{text "|"} & @{term "Cn n r rs"} & (composition)\\
+ @{text "|"} & @{term "Pr n r\<^isub>1 r\<^isub>2"} & (primitive recursion)\\
+ @{text "|"} & @{term "Mn n r"} & (minimisation)\\
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+
+ \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
+ 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
+ universal function (we refer the reader to our formalisation).
+
*}
(*
@@ -1275,7 +1322,7 @@
section {* Conclusion *}
text {*
- We have formalised the main results from three chapters in the
+ We have formalised the main results from six chapters in the
textbook by Boolos et al \cite{Boolos87}. Following in the
footsteps of another paper \cite{Nipkow98} formalising the results
from a semantics textbook, we could have titled our paper ``Boolos et al are
@@ -1351,7 +1398,9 @@
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
- programs.
+ 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/}
*}