388 text {*

   389   \noindent

   390   Boolos et al \cite{Boolos87} use abacus machines as a 

   391   stepping stone for making it less laborious to write

   392   programs for Turing machines. Abacus machines operate

   393   over an unlimited number of registers $R_0$, $R_1$, \ldots

   394   each being able to hold an arbitrary large natural number.

   395   We use natural numbers to refer to registers and also

   396   to \emph{opcodes} of abacus machines. Obcodes are

   397   defined as the datatype

   398 

   399   \begin{center}

   400   \begin{tabular}{rcll}

   401   @{text "o"} & $::=$  & @{term "Inc R"} & increment register $R$ by one\\

   402   & $\mid$ & @{term "Dec R o"} & if content of $R$ is non-zero, then decrement it by one\\

   403   & & & otherwise jump to opcode $o$

   404   & $\mid$ & @{term "Goto o"} & jump to opcode $o$

   405   \end{tabular}

   406   \end{center}

   407 *}

   408 

   409