
diff -r 1ce74a77fa2a -r 0b302c0b449a Paper/Paper.thy
--- 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/}
 *}




