tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:1ce74a77fa2a
+:0b302c0b449a
 (*<*)
 theory Paper
-imports "../thys/abacus"
+imports "../thys/recursive"
 begin
-(*
 hide_const (open) s
-*)
 hide_const (open) Divides.adjust
 abbreviation
 inv_loop0 ("J\<^isub>0") and
 inv_end1 ("K\<^isub>1") and
 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:
 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
 using assms by auto
 lemma layout:
 shows "layout_of [] = []"
-and   "layout_of ((Inc R\<iota>)#os) = (2 * R\<iota> + 9)#(layout_of os)"
+and   "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)"
-and   "layout_of ((Dec R\<iota> i)#os) = (2 * R\<iota> + 16)#(layout_of os)"
+and   "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)"
-and   "layout_of ((Goto i)#os) = 1#(layout_of os)"
+and   "layout_of ((Goto l)#is) = 1#(layout_of is)"
 by(auto simp add: layout_of.simps length_of.simps)
 (*>*)
 In this paper we take on this daunting prospect and provide a
 formalisation of Turing machines, as well as abacus machines (a kind
 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
 fortunately quite often), but also tackle the more complicated case
 when we translate abacus programs into Turing programs.  This
 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
-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
 recursive functions to abacus machines, the textbook again only shows
 how it can be done for 2- and 3-ary functions, but in the
 \label{dither}
 \end{equation}
 %
 \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
 case of reading @{term Oc}. We have the convention that the first
 state is always the \emph{starting state} of the Turing machine.
 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
 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{equation}
-\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+\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}
 \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)}
-\end{tabular}
+\end{tabular}}\label{standard}
-\end{center}
+\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.
 Before we can prove the undecidability of the halting problem for
 our Turing machines working on standard tapes, we have to analyse
 "tcopy_end"}.
 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.
 \begin{center}
 \begin{tabular}{l@ {\hspace{3mm}}lcl}
 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 "(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.
 \begin{center}
 \end{tabular}
 \end{center}
 \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
 for @{term "tcopy_begin"}.
 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
 account and is calculated according to the following measure function:
 \noindent
 With this in place, we can show that for every starting tape of the
 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}
 @{thm (concl) begin_correct}\hspace{6mm}
 @{thm (concl) loop_correct}\hspace{6mm}
 @{thm (concl) end_correct}
 \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
 n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
 n"}, we can derive the following Hoare-triple for the correctness
 This roughly means we considering only Turing machine programs
 representing functions that take some numbers as input and produce a
 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
 represents a Turing machine @{term "M"} as a natural number.  No
 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}:
 \begin{center}
 \begin{center}
 @{thm tcontra_def}
 \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
 \begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}}
 \begin{tabular}[t]{@ {}l@ {}}
 \noindent
 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
 \begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}}
 \begin{tabular}[t]{@ {}l@ {}}
 \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 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.
 *}
 text {*
 \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$,
+programs. Abacus machines operate over a set of registers @{text "R\<^isub>0"},
-$R_1$, \ldots{} each being able to hold an arbitrary large natural
+@{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\\
+& $\mid$ & @{term "Dec R\<iota> l"} & if content of $R$ is non-zero, then decrement it by one\\
-& & & otherwise jump to instruction $i$\\
+& & & otherwise jump to instruction $l$\\
-& $\mid$ & @{term "Goto i"} & jump to instruction $i$
+& $\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
 this way it is again easy to define a function @{term steps} that
 executes @{term n} instructions of an abacus program. A \emph{configuration}
 of an abacus machine is the current program counter together with a snapshot of
 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
+standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it
-seems difficult to build a Turing machine programs out of components
+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
 \begin{center}
 \end{tabular}
 \end{center}
 \noindent
 This gives us a list of natural numbers specifying how many states
-are needed to translate each abacus instruction. The @{text Goto}
+are needed to translate each abacus instruction. This information
-instruction is easiest to translate requiring only one state in
+is needed in order to calculate the state where the Turing program
-the corresponding Turing machine:
+code of one abacus instruction ends.
+The @{text Goto}
-\begin{center}
+instruction is easiest to translate requiring only one state, namely
-@{thm (rhs) tgoto.simps[where n="i"]}
+the Turing machine program:
-\end{center}
+\begin{center}
-\noindent
+@{text "tm_of_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]}
-where @{term "i"} is the state in the Turing machine program
+\end{center}
-to jump to. For translating the instruction @{term Inc},
+\noindent
+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
+in the Turing machine as a standard tape. Therefore the translated Turing machine
-needs to first find the number corresponding to the register @{text "R"}. This needs a 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}
 \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\
 \end{center}
 \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).
 Finally, having a Turing machine for each abacus instruction we need
 to ``stitch'' the Turing machines together into one so that each
 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
 that for each configuration of an abacus machine the @{term
 step}-function is simulated by zero or more steps in our translated
 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).
 *}
 (*
 section {* Wang Tiles\label{Wang} *}
 *)
 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
 (almost) Right''. We have not attempted to formalise everything
 precisely as Boolos et al present it, but use definitions that make
 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
-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/}
 *}

changeset 126	0b302c0b449a
parent 125	1ce74a77fa2a
child 129	c3832c4963c4