1194   last register (the one with the highest index in the program).

  1194   last register (the one with the highest index in the program).

  1195   

  1195   

  1196   The main point of abacus programs is to be able to translate them to 

  1196   The main point of abacus programs is to be able to translate them to 

  1197   Turing machine programs. Registers and their content are represented by

  1197   Turing machine programs. Registers and their content are represented by

  1198   standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it

  1198   standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it

  1200   using our @{text "\<oplus>"}-operation shown in the previous section.

  1200   using our @{text "\<oplus>"}-operation shown in the previous section.

  1201   To overcome this difficulty, we calculate a \emph{layout} of an

  1201   To overcome this difficulty, we calculate a \emph{layout} of an

  1202   abacus program as follows

  1202   abacus program as follows

  1203 

  1203 

  1204   \begin{center}

  1204   \begin{center}

  1248   Finally, we need to transition the head of the

  1248   Finally, we need to transition the head of the

  1249   Turing machine back into the standard position. This requires a Turing machine

  1249   Turing machine back into the standard position. This requires a Turing machine

  1250   with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the 

  1250   with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the 

  1251   translated Turing machine needs to first check whether the content of the

  1251   translated Turing machine needs to first check whether the content of the

  1252   corresponding register is @{text 0}. For this we have a Turing machine program

  1252   corresponding register is @{text 0}. For this we have a Turing machine program

  1254 

  1254 

  1255   Finally, having a Turing machine for each abacus instruction we need

  1255   Finally, having a Turing machine for each abacus instruction we need

  1256   to ``stitch'' the Turing machines together into one so that each

  1256   to ``stitch'' the Turing machines together into one so that each

  1257   Turing machine component transitions to next one, just like in

  1257   Turing machine component transitions to next one, just like in

  1258   the abacus programs. One last problem to overcome is that an abacus

  1258   the abacus programs. One last problem to overcome is that an abacus

  1402   containing the inconsistency was introduced in the fourth edition

  1402   containing the inconsistency was introduced in the fourth edition

  1403   \cite{BoolosFourth}). The central

  1403   \cite{BoolosFourth}). The central

  1404   idea about Turing machines is that when started with standard tapes

  1404   idea about Turing machines is that when started with standard tapes

  1405   they compute a partial arithmetic function.  The inconsitency arises

  1405   they compute a partial arithmetic function.  The inconsitency arises

  1406   when they define the case when this function should \emph{not} return a

  1406   when they define the case when this function should \emph{not} return a

  1408 

  1408 

  1409   \begin{quote}\it

  1409   \begin{quote}\it

  1410   ``If the function that is to be computed assigns no value to the arguments that 

  1410   ``If the function that is to be computed assigns no value to the arguments that 

  1411   are represented initially on the tape, then the machine either will never halt, 

  1411   are represented initially on the tape, then the machine either will never halt, 

  1412   \colorbox{mygrey}{or} will halt in some nonstandard configuration\ldots''

  1412   \colorbox{mygrey}{or} will halt in some nonstandard configuration\ldots''

  1569   one wants to undertake too many times (our formalisation of abacus

  1569   one wants to undertake too many times (our formalisation of abacus

  1570   machines and their correct translation is approximately 4600 loc;

  1570   machines and their correct translation is approximately 4600 loc;

  1571   recursive functions 5000 loc and the universal Turing machine 10000 loc).

  1571   recursive functions 5000 loc and the universal Turing machine 10000 loc).

  1572   

  1572   

  1573   Our work is also very much inspired by the formalisation of Turing

  1573   Our work is also very much inspired by the formalisation of Turing

  1575   Matita theorem prover. It turns out that their notion of

  1575   Matita theorem prover. It turns out that their notion of

  1576   realisability and our Hoare-triples are very similar, however we

  1576   realisability and our Hoare-triples are very similar, however we

  1577   differ in some basic definitions for Turing machines. Asperti and

  1577   differ in some basic definitions for Turing machines. Asperti and

  1578   Ricciotti are interested in providing a mechanised foundation for

  1578   Ricciotti are interested in providing a mechanised foundation for

  1579   complexity theory. They formalised a universal Turing machine

  1579   complexity theory. They formalised a universal Turing machine