211 In this paper we take on this daunting prospect and provide a |
211 In this paper we take on this daunting prospect and provide a |
212 formalisation of Turing machines, as well as abacus machines (a kind |
212 formalisation of Turing machines, as well as abacus machines (a kind |
213 of register machines) and recursive functions. To see the difficulties |
213 of register machines) and recursive functions. To see the difficulties |
214 involved with this work, one has to understand that Turing machine |
214 involved with this work, one has to understand that Turing machine |
215 programs can be completely \emph{unstructured}, behaving similar to |
215 programs can be completely \emph{unstructured}, behaving similar to |
216 Basic programs involving the infamous goto \cite{Dijkstra68}. This |
216 Basic programs containing the infamous goto-statement \cite{Dijkstra68}. This |
217 precludes in the general case a compositional Hoare-style reasoning |
217 precludes in the general case a compositional Hoare-style reasoning |
218 about Turing programs. We provide such Hoare-rules for when it |
218 about Turing programs. We provide such Hoare-rules for when it |
219 \emph{is} possible to reason in a compositional manner (which is |
219 \emph{is} possible to reason in a compositional manner (which is |
220 fortunately quite often), but also tackle the more complicated case |
220 fortunately quite often), but also tackle the more complicated case |
221 when we translate abacus programs into Turing programs. This |
221 when we translate abacus programs into Turing programs. This |
1189 |
1189 |
1190 |
1190 |
1191 section {* Related Work *} |
1191 section {* Related Work *} |
1192 |
1192 |
1193 text {* |
1193 text {* |
1194 The most closely related work is by Norrish \cite{Norrish11}, and Asperti and |
1194 We have formalised the main results from three chapters in the |
1195 Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on |
1195 textbook by Boolos et al \cite{Boolos87}. Following in the |
1196 lambda-terms. For this he introduced a clever rewriting technology |
1196 footsteps of another paper \cite{Nipkow98} formalising the results |
1197 based on combinators and de-Bruijn indices for |
1197 from a textbook, we could have titled our paper ``Boolos et al are |
1198 rewriting modulo $\beta$-equivalence (to keep it manageable) |
1198 (almost) Right''. We have not attempted to formalise everything |
1199 |
1199 precisely as Boolos et al present it, but find definitions that make |
1200 |
1200 mechanised proofs manageable. We have found a small inconsitency in |
1201 |
1201 the usage of definitions of \ldots Our interest in this subject |
1202 Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program |
1202 arose from correctness proofs about algorithms where we were unable |
1203 @{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"} |
1203 to formalise argumants about decidability. |
1204 |
1204 |
1205 \begin{center} |
1205 |
1206 \begin{tabular}{l} |
1206 The most closely related work is by Norrish \cite{Norrish11}, and |
1207 @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\ |
1207 Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his |
1208 \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"} |
1208 approach on lambda-terms. For this he introduced a clever rewriting |
1209 \end{tabular} |
1209 technology based on combinators and de-Bruijn indices for rewriting |
1210 \end{center} |
1210 modulo $\beta$-equivalence (to keep it manageable) |
1211 |
1211 |
1212 \noindent |
1212 |
1213 where @{text 1} stands for the starting state and @{text 0} for our final state. |
|
1214 A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff |
|
1215 |
|
1216 \begin{center} |
|
1217 @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv> |
|
1218 \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} |
|
1219 \end{center} |
|
1220 |
1213 |
1221 \noindent |
1214 \noindent |
1222 Later on we need to consider specific Turing machines that |
1215 Later on we need to consider specific Turing machines that |
1223 start with a tape in standard form and halt the computation |
1216 start with a tape in standard form and halt the computation |
1224 in standard form. To define a tape in standard form, it is |
1217 in standard form. To define a tape in standard form, it is |
1225 useful to have an operation %@{ term "tape_of_nat_list DUMMY"} |
1218 useful to have an operation %@{ term "tape_of_nat_list DUMMY"} |
1226 that translates lists of natural numbers into tapes. |
1219 that translates lists of natural numbers into tapes. |
1227 |
1220 |
1228 |
1221 |
1229 \begin{center} |
|
1230 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
1231 %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\ |
|
1232 %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\ |
|
1233 %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\ |
|
1234 \end{tabular} |
|
1235 \end{center} |
|
1236 |
|
1237 |
|
1238 By this we mean |
|
1239 |
|
1240 \begin{center} |
|
1241 %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]} |
|
1242 \end{center} |
|
1243 |
|
1244 \noindent |
1222 \noindent |
1245 This means the Turing machine starts with a tape containg @{text n} @{term Oc}s |
1223 This means the Turing machine starts with a tape containg @{text n} @{term Oc}s |
1246 and the head pointing to the first one; the Turing machine |
1224 and the head pointing to the first one; the Turing machine |
1247 halts with a tape consisting of some @{term Bk}s, followed by a |
1225 halts with a tape consisting of some @{term Bk}s, followed by a |
1248 ``cluster'' of @{term Oc}s and after that by some @{term Bk}s. |
1226 ``cluster'' of @{term Oc}s and after that by some @{term Bk}s. |