# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360055826 0
# Node ID 892a3d7493aaef679b552192e6f7f7219bd2e940
# Parent  7d8a1bfb89253dc880f9a4b6db72d6327a946d18
updated

diff -r 7d8a1bfb8925 -r 892a3d7493aa Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Feb 05 08:58:30 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 09:17:06 2013 +0000
@@ -1170,7 +1170,9 @@
   Turing machines, we fetch instructions from an abacus program such
   that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
   this way it is easy to define a function @{term steps} that
-  executes @{term n} instructions of an abacus program.
+  executes @{term n} instructions of an abacus program. By convention
+  the value calculated by an abacus program is stored in the
+  last register (the register with the highest index).
   
   The main point of abacus programs is to be able to translate them to 
   Turing machine programs. Registers and their content are represented by
@@ -1229,8 +1231,13 @@
   Finally, having a turing machine for each abacus instruction we need
   to ``stitch'' the Turing machines together into one so that each
   Turing machine component transitions to next one, just like in
-  are needed to translate each abacus instructionabacus
-  programs. While generating the Turing machine program for an abacus
+  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
+  ``mops up'' the tape (cleaning all @{text Oc}s) except for the
+  last number represented on the tape.
+
+  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
   are needed to translate each abacus instructionthat we cannot
diff -r 7d8a1bfb8925 -r 892a3d7493aa paper.pdf
Binary file paper.pdf has changed