diff -r 251e192339b7 -r 559e5c6e5113 Paper/Paper.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/Paper.thy Fri Jan 18 11:40:01 2013 +0000 @@ -0,0 +1,610 @@ +(*<*) +theory Paper +imports "../thys/uncomputable" +begin + +(* +hide_const (open) s +*) + +abbreviation + "update2 p a \ update a p" + +consts DUMMY::'a + +notation (latex output) + Cons ("_::_" [78,77] 73) and + set ("") and + W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and + W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and + update2 ("update") and +(* abc_lm_v ("lookup") and + abc_lm_s ("set") and*) + haltP ("stdhalt") and + tcopy ("copy") and + tape_of_nat_list ("\_\") and + tm_comp ("_ \ _") and + DUMMY ("\<^raw:\mbox{$\_$}>") + +declare [[show_question_marks = false]] +(*>*) + +section {* Introduction *} + +text {* + +\noindent +We formalised in earlier work the correctness proofs for two +algorithms in Isabelle/HOL---one about type-checking in +LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests +in access control~\cite{WuZhangUrban12}. The formalisations +uncovered a gap in the informal correctness proof of the former and +made us realise that important details were left out in the informal +model for the latter. However, in both cases we were unable to +formalise in Isabelle/HOL computability arguments about the +algorithms. The reason is that both algorithms are formulated in terms +of inductive predicates. Suppose @{text "P"} stands for one such +predicate. Decidability of @{text P} usually amounts to showing +whether \mbox{@{term "P \ \P"}} holds. But this does \emph{not} work +in Isabelle/HOL, since it is a theorem prover based on classical logic +where the law of excluded middle ensures that \mbox{@{term "P \ \P"}} +is always provable no matter whether @{text P} is constructed by +computable means. The same problem would arise if we had formulated +the algorithms as recursive functions, because internally in +Isabelle/HOL, like in all HOL-based theorem provers, functions are +represented as inductively defined predicates too. + +The only satisfying way out of this problem in a theorem prover based on classical +logic is to formalise a theory of computability. Norrish provided such +a formalisation for the HOL4 theorem prover. He choose the +$\lambda$-calculus as the starting point for his formalisation +of computability theory, +because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his +formalisation is a clever infrastructure for reducing +$\lambda$-terms. He also established the computational equivalence +between the $\lambda$-calculus and recursive functions. Nevertheless he +concluded that it would be ``appealing'' to have formalisations for more +operational models of computations, such as Turing machines or register +machines. One reason is that many proofs in the literature use +them. He noted however that in the context of theorem provers +\cite[Page 310]{Norrish11}: + +\begin{quote} +\it``If register machines are unappealing because of their +general fiddliness, Turing machines are an even more +daunting prospect.'' +\end{quote} + +\noindent +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 interactive +theorem provers, like Isabelle/HOL, are at their best when the +data-structures at hand are ``structurally'' defined, like lists, +natural numbers, regular expressions, etc. Such data-structures come +with convenient reasoning infrastructures (for example induction +principles, recursion combinators and so on). But this is \emph{not} +the case with Turing machines (and also not with register machines): +underlying their definitions are sets of states together with +transition functions, all of which are not structurally defined. This +means we have to implement our own reasoning infrastructure in order +to prove properties about them. This leads to annoyingly fiddly +formalisations. We noticed first the difference between both, +structural and non-structural, ``worlds'' when formalising the +Myhill-Nerode theorem, where regular expressions fared much better +than automata \cite{WuZhangUrban11}. However, with Turing machines +there seems to be no alternative if one wants to formalise the great +many proofs from the literature that use them. We will analyse one +example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The +standard proof of this property uses the notion of universal +Turing machines. + +We are not the first who formalised Turing machines in a theorem +prover: we are aware of the preliminary work by Asperti and Ricciotti +\cite{AspertiRicciotti12}. They describe a complete formalisation of +Turing machines in the Matita theorem prover, including a universal +Turing machine. They report that the informal proofs from which they +started are \emph{not} ``sufficiently accurate to be directly usable as a +guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For +our formalisation we followed mainly the proofs from the textbook +\cite{Boolos87} and found that the description there is quite +detailed. Some details are left out however: for example, it is only +shown 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 +formalisation we need arbitrary functions. But the general ideas for +how to do this are clear enough in \cite{Boolos87}. However, one +aspect that is completely left out from the informal description in +\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing +machines are correct. We will introduce Hoare-style proof rules +which help us with such correctness arguments of Turing machines. + +The main difference between our formalisation and the one by Asperti +and Ricciotti is that their universal Turing machine uses a different +alphabet than the machines it simulates. They write \cite[Page +23]{AspertiRicciotti12}: + +\begin{quote}\it +``In particular, the fact that the universal machine operates with a +different alphabet with respect to the machines it simulates is +annoying.'' +\end{quote} + +\noindent +In this paper we follow the approach by Boolos et al \cite{Boolos87}, +which goes back to Post \cite{Post36}, where all Turing machines +operate on tapes that contain only \emph{blank} or \emph{occupied} cells +(represented by @{term Bk} and @{term Oc}, respectively, in our +formalisation). Traditionally the content of a cell can be any +character from a finite alphabet. Although computationally equivalent, +the more restrictive notion of Turing machines in \cite{Boolos87} makes +the reasoning more uniform. In addition some proofs \emph{about} Turing +machines are simpler. The reason is that one often needs to encode +Turing machines---consequently if the Turing machines are simpler, then the coding +functions are simpler too. Unfortunately, the restrictiveness also makes +it harder to design programs for these Turing machines. In order +to construct a universal Turing machine we therefore do not follow +\cite{AspertiRicciotti12}, instead follow the proof in +\cite{Boolos87} by relating abacus machines to Turing machines and in +turn recursive functions to abacus machines. The universal Turing +machine can then be constructed as a recursive function. + +\smallskip +\noindent +{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the +description of Boolos et al \cite{Boolos87} where tapes only have blank or +occupied cells. We mechanise the undecidability of the halting problem and +prove the correctness of concrete Turing machines that are needed +in this proof; such correctness proofs are left out in the informal literature. +We construct the universal Turing machine from \cite{Boolos87} by +relating recursive functions to abacus machines and abacus machines to +Turing machines. Since we have set up in Isabelle/HOL a very general computability +model and undecidability result, we are able to formalise the +undecidability of Wang's tiling problem. We are not aware of any other +formalisation of a substantial undecidability problem. +*} + +section {* Turing Machines *} + +text {* \noindent + Turing machines can be thought of as having a read-write-unit, also + referred to as \emph{head}, + ``gliding'' over a potentially infinite tape. Boolos et + al~\cite{Boolos87} only consider tapes with cells being either blank + or occupied, which we represent by a datatype having two + constructors, namely @{text Bk} and @{text Oc}. One way to + represent such tapes is to use a pair of lists, written @{term "(l, + r)"}, where @{term l} stands for the tape on the left-hand side of the + head and @{term r} for the tape on the right-hand side. We 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 operates. This can + be pictured as follows: + + \begin{center} + \begin{tikzpicture} + \draw[very thick] (-3.0,0) -- ( 3.0,0); + \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5); + \draw[very thick] (-0.25,0) -- (-0.25,0.5); + \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); + \draw[very thick] (-0.75,0) -- (-0.75,0.5); + \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); + \draw[very thick] (-1.25,0) -- (-1.25,0.5); + \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); + \draw[very thick] (-1.75,0) -- (-1.75,0.5); + \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); + \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); + \draw[fill] (1.35,0.1) rectangle (1.65,0.4); + \draw[fill] (0.85,0.1) rectangle (1.15,0.4); + \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); + \draw (-0.25,0.8) -- (-0.25,-0.8); + \draw[<->] (-1.25,-0.7) -- (0.75,-0.7); + \node [anchor=base] at (-0.8,-0.5) {\small left list}; + \node [anchor=base] at (0.35,-0.5) {\small right list}; + \node [anchor=base] at (0.1,0.7) {\small head}; + \node [anchor=base] at (-2.2,0.2) {\ldots}; + \node [anchor=base] at ( 2.3,0.2) {\ldots}; + \end{tikzpicture} + \end{center} + + \noindent + Note that by using lists each side of the tape is only finite. The + potential infinity is achieved by adding an appropriate blank or occupied cell + whenever the head goes over the ``edge'' of the tape. To + make this formal we define five possible \emph{actions} + the Turing machine can perform: + + \begin{center} + \begin{tabular}{rcll} + @{text "a"} & $::=$ & @{term "W0"} & write blank (@{term Bk})\\ + & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\ + & $\mid$ & @{term L} & move left\\ + & $\mid$ & @{term R} & move right\\ + & $\mid$ & @{term Nop} & do-nothing operation\\ + \end{tabular} + \end{center} + + \noindent + We slightly deviate + from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use + will become important when we formalise halting computations and also universal Turing + machines. Given a tape and an action, we can define the + following tape updating function: + + \begin{center} + \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + @{thm (lhs) update.simps(1)} & @{text "\"} & @{thm (rhs) update.simps(1)}\\ + @{thm (lhs) update.simps(2)} & @{text "\"} & @{thm (rhs) update.simps(2)}\\ + @{thm (lhs) update.simps(3)} & @{text "\"} & \\ + \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) update.simps(3)}}\\ + @{thm (lhs) update.simps(4)} & @{text "\"} & \\ + \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) update.simps(4)}}\\ + @{thm (lhs) update.simps(5)} & @{text "\"} & @{thm (rhs) update.simps(5)}\\ + \end{tabular} + \end{center} + + \noindent + The first two clauses replace the head of the right-list + with a new @{term Bk} or @{term Oc}, respectively. To see that + these two clauses make sense in case where @{text r} is the empty + list, one has to know that the tail function, @{term tl}, is defined in + Isabelle/HOL + such that @{term "tl [] == []"} holds. The third clause + implements the move of the head one step to the left: we need + to test if the left-list @{term l} is empty; if yes, then we just prepend a + blank cell to the right-list; otherwise we have to remove the + head from the left-list and prepend it to the right-list. Similarly + in the fourth clause for a right move action. The @{term Nop} operation + leaves the the tape unchanged (last clause). + + Note that our treatment of the tape is rather ``unsymmetric''---we + have the convention that the head of the right-list is where the + head is currently positioned. Asperti and Ricciotti + \cite{AspertiRicciotti12} also considered such a representation, but + dismiss it as it complicates their definition for \emph{tape + equality}. The reason is that moving the head one step to + the left and then back to the right might change the tape (in case + of going over the ``edge''). Therefore they distinguish four types + of tapes: one where the tape is empty; another where the head + is on the left edge, respectively right edge, and in the middle + of the tape. The reading, writing and moving of the tape is then + defined in terms of these four cases. In this way they can keep the + tape in a ``normalised'' form, and thus making a left-move followed + by a right-move being the identity on tapes. Since we are not using + the notion of tape equality, we can get away with the unsymmetric + definition above, and by using the @{term update} function + cover uniformly all cases including corner cases. + + Next we need to define the \emph{states} of a Turing machine. Given + how little is usually said about how to represent them in informal + presentations, it might be surprising that in a theorem prover we + have to select carefully a representation. If we use the naive + representation where a Turing machine consists of a finite set of + states, then we will have difficulties composing two Turing + machines: we would need to combine two finite sets of states, + possibly renaming states apart whenever both machines share + states.\footnote{The usual disjoint union operation in Isabelle/HOL + cannot be used as it does not preserve types.} This renaming can be + quite cumbersome to reason about. Therefore we made the choice of + representing a state by a natural number and the states of a Turing + machine will always consist of the initial segment of natural + numbers starting from @{text 0} up to the number of states of the + machine. In doing so we can compose two Turing machine by + shifting the states of one by an appropriate amount to a higher + segment and adjusting some ``next states'' in the other. + + An \emph{instruction} @{term i} of a Turing machine is a pair consisting of + an action and a natural number (the next state). A \emph{program} @{term p} of a Turing + machine is then a list of such pairs. Using as an example the following Turing machine + program, which consists of four instructions + + \begin{equation} + \begin{tikzpicture} + \node [anchor=base] at (0,0) {@{thm dither_def}}; + \node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$}; + \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$}; + \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$}; + \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$}; + \end{tikzpicture} + \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 the + 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. + The zeroth state is special in that it will be used as the + ``halting state''. There are no instructions for the @{text + 0}-state, but it will always perform a @{term Nop}-operation and + remain in the @{text 0}-state. Unlike Asperti and Riccioti + \cite{AspertiRicciotti12}, we have chosen a very concrete + representation for programs, because when constructing a universal + Turing machine, we need to define a coding function for programs. + This can be easily done for our programs-as-lists, but is more + difficult for the functions used by Asperti and Ricciotti. + + Given a program @{term p}, a state + and the cell being read by the head, we need to fetch + the corresponding instruction from the program. For this we define + the function @{term fetch} + + \begin{center} + \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + \multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\ + @{thm (lhs) fetch.simps(2)} & @{text "\"} & \\ + \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\ + \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \ (Nop, 0) |"}}\\ + \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \ i"}}\\ + @{thm (lhs) fetch.simps(3)} & @{text "\"} & \\ + \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\ + \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \ (Nop, 0) |"}}\\ + \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \ i"}} + \end{tabular} + \end{center} + + \noindent + In this definition the function @{term nth_of} returns the @{text n}th element + from a list, provided it exists (@{term Some}-case), or if it does not, it + returns the default action @{term Nop} and the default state @{text 0} + (@{term None}-case). In doing so we slightly deviate from the description + in \cite{Boolos87}: if their Turing machines transition to a non-existing + state, then the computation is halted. We will transition in such cases + to the @{text 0}-state. However, with introducing the + notion of \emph{well-formed} Turing machine programs we will later exclude such + cases and make the @{text 0}-state the only ``halting state''. A program + @{term p} is said to be well-formed if it satisfies + the following three properties: + + \begin{center} + \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + @{term "t_correct p"} & @{text "\"} & @{term "2 <= length p"}\\ + & @{text "\"} & @{term "iseven (length p)"}\\ + & @{text "\"} & @{term "\ (a, s) \ set p. s <= length p div 2"} + \end{tabular} + \end{center} + + \noindent + The first says that @{text p} must have at least an instruction for the starting + state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every + state, and the third that every next-state is one of the states mentioned in + the program or being the @{text 0}-state. + + A \emph{configuration} @{term c} of a Turing machine is a state together with + a tape. This is written as @{text "(s, (l, r))"}. If we have a + configuration and a program, we can calculate + what the next configuration is by fetching the appropriate action and next state + from the program, and by updating the state and tape accordingly. + This single step of execution is defined as the function @{term tstep} + + \begin{center} + \begin{tabular}{l} + @{text "step (s, (l, r)) p"} @{text "\"}\\ + \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\ + \hspace{10mm}@{text "in (s', update (l, r) a)"} + \end{tabular} + \end{center} + + \noindent + where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is + empty it returns @{term Bk}. + It is impossible in Isabelle/HOL to lift the @{term step}-function realising + a general evaluation function for Turing machines. The reason is that functions in HOL-based + provers need to be terminating, and clearly there are Turing machine + programs that are not. We can however define an evaluation + function so that it performs exactly @{text n} steps: + + \begin{center} + \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + @{thm (lhs) steps.simps(1)} & @{text "\"} & @{thm (rhs) steps.simps(1)}\\ + @{thm (lhs) steps.simps(2)} & @{text "\"} & @{thm (rhs) steps.simps(2)}\\ + \end{tabular} + \end{center} + + \noindent + Recall our definition of @{term fetch} with the default value for + the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less + then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation + does not actually halt, but rather transitions to the @{text 0}-state and + remains there performing @{text Nop}-actions until @{text n} is reached. + + Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program + @{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"} + + \begin{center} + \begin{tabular}{l} + @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\"}\\ + \hspace{6mm}@{text "\n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"} + \end{tabular} + \end{center} + + \noindent + where @{text 1} stands for the starting state and @{text 0} for our final state. + A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff + + \begin{center} + @{term "halts p (l\<^isub>i, r\<^isub>i) \ + \l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} + \end{center} + + \noindent + Later on we need to consider specific Turing machines that + start with a tape in standard form and halt the computation + in standard form. To define a tape in standard form, it is + useful to have an operation %@{ term "tape_of_nat_list DUMMY"} + that translates lists of natural numbers into tapes. + + + \begin{center} + \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\ + %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\ + %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\ + \end{tabular} + \end{center} + + + + + By this we mean + + \begin{center} + %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]} + \end{center} + + \noindent + This means the Turing machine starts with a tape containg @{text n} @{term Oc}s + and the head pointing to the first one; the Turing machine + halts with a tape consisting of some @{term Bk}s, followed by a + ``cluster'' of @{term Oc}s and after that by some @{term Bk}s. + The head in the output is pointing again at the first @{term Oc}. + The intuitive meaning of this definition is to start the Turing machine with a + tape corresponding to a value @{term n} and producing + a new tape corresponding to the value @{term l} (the number of @{term Oc}s + clustered on the output tape). + + Before we can prove the undecidability of the halting problem for Turing machines, + we have to define how to compose two Turing machines. Given our setup, this is + relatively straightforward, if slightly fiddly. We use the following two + auxiliary functions: + + \begin{center} + \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} + @{thm (lhs) shift.simps} @{text "\"}\\ + \hspace{4mm}@{thm (rhs) shift.simps}\\ + @{thm (lhs) adjust.simps} @{text "\"}\\ + \hspace{4mm}@{text "map (\ (a, s)."}\\ + \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\ + \end{tabular} + \end{center} + + \noindent + The first adds @{text n} to all states, exept the @{text 0}-state, + thus moving all ``regular'' states to the segment starting at @{text + n}; the second adds @{term "length p div 2 + 1"} to the @{text + 0}-state, thus ridirecting all references to the ``halting state'' + to the first state after the program @{text p}. With these two + functions in place, we can define the \emph{sequential composition} + of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} + + \begin{center} + @{thm tm_comp.simps[THEN eq_reflection]} + \end{center} + + \noindent + This means @{text "p\<^isub>1"} is executed first. Whenever it originally + transitioned to the @{text 0}-state, it will in the composed program transition to the starting + state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"} + have been shifted in order to make sure that the states of the composed + program @{text "p\<^isub>1 \ p\<^isub>2"} still only ``occupy'' + an initial segment of the natural numbers. + + \begin{center} + \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}} + @{thm (lhs) tcopy_def} & @{text "\"} & @{thm (rhs) tcopy_def} + \end{tabular} + \end{center} + + + assertion holds for all tapes + + Hoare rule for composition + + For showing the undecidability of the halting problem, we need to consider + two specific Turing machines. copying TM and dithering TM + + correctness of the copying TM + + measure for the copying TM, which we however omit. + + halting problem +*} + +section {* Abacus Machines *} + +text {* + \noindent + Boolos et al \cite{Boolos87} use abacus machines as a + stepping stone for making it less laborious to write + programs for Turing machines. Abacus machines operate + over an unlimited number of registers $R_0$, $R_1$, \ldots + each being able to hold an arbitrary large natural number. + We use natural numbers to refer to registers, but also + to refer to \emph{opcodes} of abacus + machines. Obcodes are given by the datatype + + \begin{center} + \begin{tabular}{rcll} + @{text "o"} & $::=$ & @{term "Inc R\"} & increment register $R$ by one\\ + & $\mid$ & @{term "Dec R\ o\"} & if content of $R$ is non-zero,\\ + & & & then decrement it by one\\ + & & & otherwise jump to opcode $o$\\ + & $\mid$ & @{term "Goto o\"} & jump to opcode $o$ + \end{tabular} + \end{center} + + \noindent + A \emph{program} of an abacus machine is a list of such + obcodes. For example the program clearing the register + $R$ (setting it to 0) can be defined as follows: + + \begin{center} + %@ {thm clear.simps[where n="R\" and e="o\", THEN eq_reflection]} + \end{center} + + \noindent + The second opcode @{term "Goto 0"} in this programm means we + jump back to the first opcode, namely @{text "Dec R o"}. + The \emph{memory} $m$ of an abacus machine holding the values + of the registers is represented as a list of natural numbers. + We have a lookup function for this memory, written @{term "abc_lm_v m R\"}, + which looks up the content of register $R$; if $R$ + is not in this list, then we return 0. Similarly we + have a setting function, written @{term "abc_lm_s m R\ n"}, which + sets the value of $R$ to $n$, and if $R$ was not yet in $m$ + it pads it approriately with 0s. + + + Abacus machine halts when it jumps out of range. +*} + + +section {* Recursive Functions *} + +section {* Wang Tiles\label{Wang} *} + +text {* + Used in texture mapings - graphics +*} + + +section {* Related Work *} + +text {* + The most closely related work is by Norrish \cite{Norrish11}, and Asperti and + Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on + lambda-terms. For this he introduced a clever rewriting technology + based on combinators and de-Bruijn indices for + rewriting modulo $\beta$-equivalence (to keep it manageable) +*} + + +(* +Questions: + +Can this be done: Ackerman function is not primitive +recursive (Nora Szasz) + +Tape is represented as two lists (finite - usually infinite tape)? + +*) + + +(*<*) +end +(*>*) \ No newline at end of file