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 decide |
1121 whether Turing machines terminate. |
1121 whether Turing machines terminate. |
1122 |
|
1123 |
|
1124 |
|
1125 *} |
1122 *} |
1126 |
1123 |
1127 |
1124 |
1128 section {* Abacus Machines *} |
1125 section {* Abacus Machines *} |
1129 |
1126 |
1133 stepping stone for making it less laborious to write |
1130 stepping stone for making it less laborious to write |
1134 programs for Turing machines. Abacus machines operate |
1131 programs for Turing machines. Abacus machines operate |
1135 over an unlimited number of registers $R_0$, $R_1$, \ldots |
1132 over an unlimited number of registers $R_0$, $R_1$, \ldots |
1136 each being able to hold an arbitrary large natural number. |
1133 each being able to hold an arbitrary large natural number. |
1137 We use natural numbers to refer to registers, but also |
1134 We use natural numbers to refer to registers, but also |
1138 to refer to \emph{opcodes} of abacus |
1135 to refer to \emph{statements} of abacus programs. Statements |
1139 machines. Obcodes are given by the datatype |
1136 are given by the datatype |
1140 |
1137 |
1141 \begin{center} |
1138 \begin{center} |
1142 \begin{tabular}{rcll} |
1139 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
1143 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1140 @{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\ |
1144 & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\ |
1141 & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\ |
1145 & & & then decrement it by one\\ |
1142 & & & then decrement it by one\\ |
1146 & & & otherwise jump to opcode $o$\\ |
1143 & & & otherwise jump to statement $o$\\ |
1147 & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$ |
1144 & $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$ |
1148 \end{tabular} |
1145 \end{tabular} |
1149 \end{center} |
1146 \end{center} |
1150 |
1147 |
1151 \noindent |
1148 \noindent |
1152 A \emph{program} of an abacus machine is a list of such |
1149 A \emph{program} of an abacus machine is a list of such |
1153 obcodes. For example the program clearing the register |
1150 statements. For example the program clearing the register |
1154 $R$ (setting it to 0) can be defined as follows: |
1151 $R$ (setting it to 0) can be defined as follows: |
1155 |
1152 |
1156 \begin{center} |
1153 \begin{center} |
1157 %@ {thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
1154 %@ {thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]} |
1158 \end{center} |
1155 \end{center} |