1139 Boolos et al \cite{Boolos87} use abacus machines as a stepping stone |
1139 Boolos et al \cite{Boolos87} use abacus machines as a stepping stone |
1140 for making it less laborious to write Turing machine |
1140 for making it less laborious to write Turing machine |
1141 programs. Abacus machines operate over a set of registers $R_0$, |
1141 programs. Abacus machines operate over a set of registers $R_0$, |
1142 $R_1$, \ldots{} each being able to hold an arbitrary large natural |
1142 $R_1$, \ldots{} each being able to hold an arbitrary large natural |
1143 number. We use natural numbers to refer to registers; we also use a natural number |
1143 number. We use natural numbers to refer to registers; we also use a natural number |
1144 to represent a program counter and jumping ``addresses''. An abacus |
1144 to represent a program counter and to represent jumping ``addresses''. An abacus |
1145 program is a list of \emph{instructions} defined by the datatype: |
1145 program is a list of \emph{instructions} defined by the datatype: |
1146 |
1146 |
1147 \begin{center} |
1147 \begin{center} |
1148 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1148 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1149 @{text "i"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1149 @{text "i"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1150 & $\mid$ & @{term "Dec R\<iota> i"} & if content of $R$ is non-zero,\\ |
1150 & $\mid$ & @{term "Dec R\<iota> i"} & if content of $R$ is non-zero, then decrement it by one\\ |
1151 & & & then decrement it by one\\ |
|
1152 & & & otherwise jump to instruction $i$\\ |
1151 & & & otherwise jump to instruction $i$\\ |
1153 & $\mid$ & @{term "Goto i"} & jump to instruction $i$ |
1152 & $\mid$ & @{term "Goto i"} & jump to instruction $i$ |
1154 \end{tabular} |
1153 \end{tabular} |
1155 \end{center} |
1154 \end{center} |
1156 |
1155 |
1163 \end{center} |
1162 \end{center} |
1164 |
1163 |
1165 \noindent |
1164 \noindent |
1166 Running such a program means we start with the first instruction |
1165 Running such a program means we start with the first instruction |
1167 then execute one instructions after the other, unless there is a jump. For |
1166 then execute one instructions after the other, unless there is a jump. For |
1168 example the second instruction the jump @{term "Goto 0"} in @{term clear} means |
1167 example the second instruction @{term "Goto 0"} in @{term clear} means |
1169 we jump back to the first instruction closing the loop. Like with our |
1168 we jump back to the first instruction thereby closing the loop. Like with our |
1170 Turing machines, we fetch instructions from an abacus program such |
1169 Turing machines, we fetch instructions from an abacus program such |
1171 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1170 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1172 this way it is easy to define a function @{term steps} that |
1171 this way it is again easy to define a function @{term steps} that |
1173 executes @{term n} instructions of an abacus program. A \emph{configuration} |
1172 executes @{term n} instructions of an abacus program. A \emph{configuration} |
1174 of an abacus machine is the program counter together with a snapshot of |
1173 of an abacus machine is the current program counter together with a snapshot of |
1175 all registers. |
1174 all registers. |
1176 By convention |
1175 By convention |
1177 the value calculated by an abacus program is stored in the |
1176 the value calculated by an abacus program is stored in the |
1178 last register (the register with the highest index). |
1177 last register (the register with the highest index). |
1179 |
1178 |
1180 The main point of abacus programs is to be able to translate them to |
1179 The main point of abacus programs is to be able to translate them to |
1181 Turing machine programs. Registers and their content are represented by |
1180 Turing machine programs. Registers and their content are represented by |
1182 standard tapes. |
1181 standard tapes. Because of the jumps in abacus programs, it |
1183 Because of the jumps in abacus programs, it |
1182 seems difficult to build a Turing machine programs out of components |
1184 seems difficult to build Turing machine programs using @{text "\<oplus>"}. |
1183 using our @{text "\<oplus>"}-operation. |
1185 To overcome this difficulty, we calculate a \emph{layout} as follows |
1184 To overcome this difficulty, we calculate a \emph{layout} as follows |
1186 |
1185 |
1187 \begin{center} |
1186 \begin{center} |
1188 \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
1187 \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
1189 @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\ |
1188 @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\ |
1249 are needed to translate each abacus instruction``block'' |
1248 are needed to translate each abacus instruction``block'' |
1250 and show as invariant that it performs the same operations |
1249 and show as invariant that it performs the same operations |
1251 as the abacus program. For this we have to show that for each |
1250 as the abacus program. For this we have to show that for each |
1252 configuration of an abacus machine the @{term step}-function |
1251 configuration of an abacus machine the @{term step}-function |
1253 is simulated by zero or more steps in our constructed Turing |
1252 is simulated by zero or more steps in our constructed Turing |
1254 machine. This leads to a rather large ``monolithic'' overall |
1253 machine. This leads to a rather large ``monolithic'' |
1255 correctness proof that on the conceptual level is difficult to |
1254 correctness proof (4600 loc and 380 sublemmas) that on the conceptual |
1256 break down into smaller components. |
1255 level is difficult to break down into smaller components. |
1257 |
1256 |
1258 %We were able to simplify the proof somewhat |
1257 %We were able to simplify the proof somewhat |
1259 *} |
1258 *} |
1260 |
1259 |
1261 |
1260 |