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\)#os) = (2 * R\ + 9)#(layout_of os)" - and "layout_of ((Dec R\ i)#os) = (2 * R\ + 16)#(layout_of os)" - and "layout_of ((Goto i)#os) = 1#(layout_of os)" + and "layout_of ((Inc R\)#is) = (2 * R\ + 9)#(layout_of is)" + and "layout_of ((Dec R\ l)#is) = (2 * R\ + 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 "\"} & @{thm (rhs) nats2tape(6)}\\ @{thm (lhs) nats2tape(4)} & @{text "\"} & @{thm (rhs) nats2tape(4)}\\ \end{tabular}\hspace{6mm} @@ -737,12 +741,12 @@ @{thm (lhs) nats2tape(1)} & @{text "\"} & @{thm (rhs) nats2tape(1)}\\ @{thm (lhs) nats2tape(2)} & @{text "\"} & @{thm (rhs) nats2tape(2)}\\ @{thm (lhs) nats2tape(3)} & @{text "\"} & @{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,\[n\<^isub>1,...,n\<^isub>m]\)"} 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 \ 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 ""}. 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\"} & increment register $R$ by one\\ - & $\mid$ & @{term "Dec R\ 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\ 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\" and e="i", THEN eq_reflection]} + @{thm clear.simps[where n="R\" 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 "\"}-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 "\"} @{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\"}, 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\"} 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\ 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/} *}