(*<*)
theory Paper
imports "../thys/uncomputable"
begin
(*
hide_const (open) s
*)
abbreviation
"update2 p a \<equiv> 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 ("\<ulcorner>_\<urcorner>") and
tm_comp ("_ \<oplus> _") 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 \<or> \<not>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 \<or> \<not>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 "\<equiv>"} & @{thm (rhs) update.simps(1)}\\
@{thm (lhs) update.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(2)}\\
@{thm (lhs) update.simps(3)} & @{text "\<equiv>"} & \\
\multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) update.simps(3)}}\\
@{thm (lhs) update.simps(4)} & @{text "\<equiv>"} & \\
\multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) update.simps(4)}}\\
@{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{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 "\<equiv>"} & \\
\multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\
\multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
\multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}\\
@{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & \\
\multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\
\multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
\multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> 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 "\<equiv>"} & @{term "2 <= length p"}\\
& @{text "\<and>"} & @{term "iseven (length p)"}\\
& @{text "\<and>"} & @{term "\<forall> (a, s) \<in> 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 "\<equiv>"}\\
\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 "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\
@{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{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 "\<equiv>"}\\
\hspace{6mm}@{text "\<exists>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) \<equiv>
\<exists>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 "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
%@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
%@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { 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 "\<equiv>"}\\
\hspace{4mm}@{thm (rhs) shift.simps}\\
@{thm (lhs) adjust.simps} @{text "\<equiv>"}\\
\hspace{4mm}@{text "map (\<lambda> (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 \<oplus> 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 "\<equiv>"} & @{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\<iota>"} & increment register $R$ by one\\
& $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
& & & then decrement it by one\\
& & & otherwise jump to opcode $o$\\
& $\mid$ & @{term "Goto o\<iota>"} & 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\<iota>" and e="o\<iota>", 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\<iota>"},
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\<iota> 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
(*>*)