1128 \noindent |
1128 \noindent |
1129 Boolos et al \cite{Boolos87} use abacus machines as a stepping stone |
1129 Boolos et al \cite{Boolos87} use abacus machines as a stepping stone |
1130 for making it less laborious to write Turing machine |
1130 for making it less laborious to write Turing machine |
1131 programs. Abacus machines operate over a set of registers $R_0$, |
1131 programs. Abacus machines operate over a set of registers $R_0$, |
1132 $R_1$, \ldots{} each being able to hold an arbitrary large natural |
1132 $R_1$, \ldots{} each being able to hold an arbitrary large natural |
1133 number. We use natural numbers to refer to registers, but also to |
1133 number. We use natural numbers to refer to registers; we also use a natural number |
1134 refer to \emph{statements} of abacus programs. Statements are given |
1134 to represent a program counter. An abacus |
1135 by the datatype |
1135 program is a list of \emph{statements} defined by the datatype: |
1136 |
1136 |
1137 \begin{center} |
1137 \begin{center} |
1138 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1138 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1139 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1139 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1140 & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\ |
1140 & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\ |
1143 & $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$ |
1143 & $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$ |
1144 \end{tabular} |
1144 \end{tabular} |
1145 \end{center} |
1145 \end{center} |
1146 |
1146 |
1147 \noindent |
1147 \noindent |
1148 A \emph{program} of an abacus machine is a list of such |
1148 For example the program clearing the register $R$ (that is setting |
1149 statements. For example the program clearing the register |
1149 it to @{term "(0::nat)"}) can be defined as follows: |
1150 $R$ (setting it to @{term "(0::nat)"}) can be defined as follows: |
|
1151 |
1150 |
1152 \begin{center} |
1151 \begin{center} |
1153 @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
1152 @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
1154 \end{center} |
1153 \end{center} |
1155 |
1154 |
1156 \noindent |
1155 \noindent |
1157 The second opcode @{term "Goto 0"} in this program means we |
1156 Running such a program means we start with the first instruction |
1158 jump back to the first statement, namely @{text "Dec R o"}. |
1157 then execute statements one after the other, unless there is a jump. For |
1159 The \emph{memory} $m$ of an abacus machine holding the values |
1158 example the second statement the jump @{term "Goto 0"} in @{term clear} means |
1160 of the registers is represented as a list of natural numbers. |
1159 we jump back to the first statement closing the loop. Like with our |
1161 We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"}, |
1160 Turing machines, we fetch statements from an abacus program such |
1162 which looks up the content of register $R$; if $R$ |
1161 that a jump out of ``range'' behaves like a @{term "Nop"}-action. In |
1163 is not in this list, then we return 0. Similarly we |
1162 this way it is easy to define a function @{term steps} that |
1164 have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which |
1163 executes @{term n} statements of an abacus program. |
1165 sets the value of $R$ to $n$, and if $R$ was not yet in $m$ |
1164 |
1166 it pads it approriately with 0s. |
1165 |
1167 |
1166 |
1168 |
1167 %Running an abacus program means to start |
1169 Abacus machine halts when it jumps out of range. |
1168 %A \emph{program} of an abacus machine is a list of such |
|
1169 %statements. |
|
1170 %The \emph{memory} $m$ of an abacus machine holding the values |
|
1171 %of the registers is represented as a list of natural numbers. |
|
1172 %We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"}, |
|
1173 %which looks up the content of register $R$; if $R$ |
|
1174 %is not in this list, then we return 0. Similarly we |
|
1175 %have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which |
|
1176 %sets the value of $R$ to $n$, and if $R$ was not yet in $m$ |
|
1177 %it pads it approriately with 0s. |
|
1178 %Abacus machine halts when it jumps out of range. |
1170 *} |
1179 *} |
1171 |
1180 |
1172 |
1181 |
1173 section {* Recursive Functions *} |
1182 section {* Recursive Functions *} |
1174 |
1183 |