53 Cons ("_::_" [78,77] 73) and |
52 Cons ("_::_" [78,77] 73) and |
54 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
53 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
55 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
54 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
56 tstep ("step") and |
55 tstep ("step") and |
57 steps ("nsteps") and |
56 steps ("nsteps") and |
|
57 abc_lm_v ("lookup") and |
|
58 abc_lm_s ("set") and |
58 DUMMY ("\<^raw:\mbox{$\_$}>") |
59 DUMMY ("\<^raw:\mbox{$\_$}>") |
59 |
60 |
60 declare [[show_question_marks = false]] |
61 declare [[show_question_marks = false]] |
61 (*>*) |
62 (*>*) |
62 |
63 |
390 Boolos et al \cite{Boolos87} use abacus machines as a |
391 Boolos et al \cite{Boolos87} use abacus machines as a |
391 stepping stone for making it less laborious to write |
392 stepping stone for making it less laborious to write |
392 programs for Turing machines. Abacus machines operate |
393 programs for Turing machines. Abacus machines operate |
393 over an unlimited number of registers $R_0$, $R_1$, \ldots |
394 over an unlimited number of registers $R_0$, $R_1$, \ldots |
394 each being able to hold an arbitrary large natural number. |
395 each being able to hold an arbitrary large natural number. |
395 We use natural numbers to refer to registers and also |
396 We use natural numbers to refer to registers, but also |
396 to \emph{opcodes} of abacus machines. Obcodes are |
397 to refer to \emph{opcodes} of abacus |
397 defined as the datatype |
398 machines. Obcodes are given by the datatype |
398 |
399 |
399 \begin{center} |
400 \begin{center} |
400 \begin{tabular}{rcll} |
401 \begin{tabular}{rcll} |
401 @{text "o"} & $::=$ & @{term "Inc R"} & increment register $R$ by one\\ |
402 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
402 & $\mid$ & @{term "Dec R n"} & if content of $R$ is non-zero, then decrement it by one\\ |
403 & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\ |
|
404 & & & then decrement it by one\\ |
403 & & & otherwise jump to opcode $o$\\ |
405 & & & otherwise jump to opcode $o$\\ |
404 & $\mid$ & @{term "Goto n"} & jump to opcode $o$ |
406 & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$ |
405 \end{tabular} |
407 \end{tabular} |
406 \end{center} |
408 \end{center} |
|
409 |
|
410 \noindent |
|
411 A \emph{program} of an abacus machine is a list of such |
|
412 obcodes. For example the program clearing the register |
|
413 $R$ (setting it to 0) can be defined as follows: |
|
414 |
|
415 \begin{center} |
|
416 @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
|
417 \end{center} |
|
418 |
|
419 \noindent |
|
420 The second opcode @{term "Goto 0"} in this programm means we |
|
421 jump back to the first opcode, namely @{text "Dec R o"}. |
|
422 The \emph{memory} $m$ of an abacus machine holding the values |
|
423 of the registers is represented as a list of natural numbers. |
|
424 We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"}, |
|
425 which looks up the content of register $R$; if $R$ |
|
426 is not in this list, then we return 0. Similarly we |
|
427 have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which |
|
428 sets the value of $R$ to $n$, and if $R$ was not yet in $m$ |
|
429 it pads it approriately with 0s. |
407 *} |
430 *} |
408 |
431 |
409 |
432 |
410 section {* Recursive Functions *} |
433 section {* Recursive Functions *} |
411 |
434 |