1115 |
1115 |
1116 \noindent |
1116 \noindent |
1117 This time the Hoare-triple states that @{term tcontra} terminates |
1117 This time the Hoare-triple states that @{term tcontra} terminates |
1118 with the ``output'' @{term "<(1::nat)>"}. In both case we come |
1118 with the ``output'' @{term "<(1::nat)>"}. In both case we come |
1119 to an contradiction, which means we have to abondon our assumption |
1119 to an contradiction, which means we have to abondon our assumption |
1120 that there exists a Turing machine @{term H} which can decide |
1120 that there exists a Turing machine @{term H} which can in general decide |
1121 whether Turing machines terminate. |
1121 whether Turing machines terminate. |
1122 *} |
1122 *} |
1123 |
1123 |
1124 |
1124 |
1125 section {* Abacus Machines *} |
1125 section {* Abacus Machines *} |
1126 |
1126 |
1127 text {* |
1127 text {* |
1128 \noindent |
1128 \noindent |
1129 Boolos et al \cite{Boolos87} use abacus machines as a |
1129 Boolos et al \cite{Boolos87} use abacus machines as a stepping stone |
1130 stepping stone for making it less laborious to write |
1130 for making it less laborious to write Turing machine |
1131 programs for Turing machines. Abacus machines operate |
1131 programs. Abacus machines operate over a set of registers $R_0$, |
1132 over an unlimited number of registers $R_0$, $R_1$, \ldots |
1132 $R_1$, \ldots{} each being able to hold an arbitrary large natural |
1133 each being able to hold an arbitrary large natural number. |
1133 number. We use natural numbers to refer to registers, but also to |
1134 We use natural numbers to refer to registers, but also |
1134 refer to \emph{statements} of abacus programs. Statements are given |
1135 to refer to \emph{statements} of abacus programs. Statements |
1135 by the datatype |
1136 are given by the datatype |
|
1137 |
1136 |
1138 \begin{center} |
1137 \begin{center} |
1139 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1138 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1140 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1139 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1141 & $\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,\\ |
1146 \end{center} |
1145 \end{center} |
1147 |
1146 |
1148 \noindent |
1147 \noindent |
1149 A \emph{program} of an abacus machine is a list of such |
1148 A \emph{program} of an abacus machine is a list of such |
1150 statements. For example the program clearing the register |
1149 statements. For example the program clearing the register |
1151 $R$ (setting it to 0) can be defined as follows: |
1150 $R$ (setting it to @{term "(0::nat)"}) can be defined as follows: |
1152 |
1151 |
1153 \begin{center} |
1152 \begin{center} |
1154 %@ {thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
1153 @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
1155 \end{center} |
1154 \end{center} |
1156 |
1155 |
1157 \noindent |
1156 \noindent |
1158 The second opcode @{term "Goto 0"} in this program means we |
1157 The second opcode @{term "Goto 0"} in this program means we |
1159 jump back to the first opcode, namely @{text "Dec R o"}. |
1158 jump back to the first statement, namely @{text "Dec R o"}. |
1160 The \emph{memory} $m$ of an abacus machine holding the values |
1159 The \emph{memory} $m$ of an abacus machine holding the values |
1161 of the registers is represented as a list of natural numbers. |
1160 of the registers is represented as a list of natural numbers. |
1162 We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"}, |
1161 We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"}, |
1163 which looks up the content of register $R$; if $R$ |
1162 which looks up the content of register $R$; if $R$ |
1164 is not in this list, then we return 0. Similarly we |
1163 is not in this list, then we return 0. Similarly we |