19 Cons ("_::_" [78,77] 73) and |
19 Cons ("_::_" [78,77] 73) and |
20 set ("") and |
20 set ("") and |
21 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
21 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
22 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
22 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
23 update2 ("update") and |
23 update2 ("update") and |
|
24 tm_wf0 ("wf") and |
24 (* abc_lm_v ("lookup") and |
25 (* abc_lm_v ("lookup") and |
25 abc_lm_s ("set") and*) |
26 abc_lm_s ("set") and*) |
26 haltP ("stdhalt") and |
27 haltP ("stdhalt") and |
27 tcopy ("copy") and |
28 tcopy ("copy") and |
28 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
29 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
88 In this paper we take on this daunting prospect and provide a |
89 In this paper we take on this daunting prospect and provide a |
89 formalisation of Turing machines, as well as abacus machines (a kind |
90 formalisation of Turing machines, as well as abacus machines (a kind |
90 of register machines) and recursive functions. To see the difficulties |
91 of register machines) and recursive functions. To see the difficulties |
91 involved with this work, one has to understand that Turing machine |
92 involved with this work, one has to understand that Turing machine |
92 programs can be completely \emph{unstructured}, behaving |
93 programs can be completely \emph{unstructured}, behaving |
93 similar Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the |
94 similar to Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the |
94 general case a compositional Hoare-style reasoning about Turing |
95 general case a compositional Hoare-style reasoning about Turing |
95 programs. We provide such Hoare-rules for when it \emph{is} possible to |
96 programs. We provide such Hoare-rules for when it \emph{is} possible to |
96 reason in a compositional manner (which is fortunately quite often), but also tackle |
97 reason in a compositional manner (which is fortunately quite often), but also tackle |
97 the more complicated case when we translate abacus programs into |
98 the more complicated case when we translate abacus programs into |
98 Turing programs. These difficulties when reasoning about computability theory |
99 Turing programs. These difficulties when reasoning about computability theory |
307 %machines: we would need to combine two finite sets of states, |
308 %machines: we would need to combine two finite sets of states, |
308 %possibly renaming states apart whenever both machines share |
309 %possibly renaming states apart whenever both machines share |
309 %states.\footnote{The usual disjoint union operation in Isabelle/HOL |
310 %states.\footnote{The usual disjoint union operation in Isabelle/HOL |
310 %cannot be used as it does not preserve types.} This renaming can be |
311 %cannot be used as it does not preserve types.} This renaming can be |
311 %quite cumbersome to reason about. |
312 %quite cumbersome to reason about. |
312 We followed the choice made by \cite{AspertiRicciotti12} |
313 We followed the choice made in \cite{AspertiRicciotti12} |
313 representing a state by a natural number and the states of a Turing |
314 representing a state by a natural number and the states of a Turing |
314 machine by the initial segment of natural numbers starting from @{text 0}. |
315 machine by the initial segment of natural numbers starting from @{text 0}. |
315 In doing so we can compose two Turing machine by |
316 In doing so we can compose two Turing machine by |
316 shifting the states of one by an appropriate amount to a higher |
317 shifting the states of one by an appropriate amount to a higher |
317 segment and adjusting some ``next states'' in the other. {\it composition here?} |
318 segment and adjusting some ``next states'' in the other. {\it composition here?} |
318 |
319 |
319 An \emph{instruction} @{term i} of a Turing machine is a pair consisting of |
320 An \emph{instruction} of a Turing machine is a pair consisting of |
320 an action and a natural number (the next state). A \emph{program} @{term p} of a Turing |
321 an action and a natural number (the next state). A \emph{program} @{term p} of a Turing |
321 machine is then a list of such pairs. Using as an example the following Turing machine |
322 machine is then a list of such pairs. Using as an example the following Turing machine |
322 program, which consists of four instructions |
323 program, which consists of four instructions |
323 |
324 |
324 \begin{equation} |
325 \begin{equation} |
396 A \emph{configuration} @{term c} of a Turing machine is a state together with |
397 A \emph{configuration} @{term c} of a Turing machine is a state together with |
397 a tape. This is written as @{text "(s, (l, r))"}. If we have a |
398 a tape. This is written as @{text "(s, (l, r))"}. If we have a |
398 configuration and a program, we can calculate |
399 configuration and a program, we can calculate |
399 what the next configuration is by fetching the appropriate action and next state |
400 what the next configuration is by fetching the appropriate action and next state |
400 from the program, and by updating the state and tape accordingly. |
401 from the program, and by updating the state and tape accordingly. |
401 This single step of execution is defined as the function @{term tstep} |
402 This single step of execution is defined as the function @{term step} |
402 |
403 |
403 \begin{center} |
404 \begin{center} |
404 \begin{tabular}{l} |
405 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
405 @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\ |
406 @{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\ |
406 \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\ |
407 & & @{text "in (s', update (l, r) a)"} |
407 \hspace{10mm}@{text "in (s', update (l, r) a)"} |
|
408 \end{tabular} |
408 \end{tabular} |
409 \end{center} |
409 \end{center} |
410 |
410 |
411 \noindent |
411 \noindent |
412 where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is |
412 where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is |
536 correctness of the copying TM |
536 correctness of the copying TM |
537 |
537 |
538 measure for the copying TM, which we however omit. |
538 measure for the copying TM, which we however omit. |
539 |
539 |
540 halting problem |
540 halting problem |
|
541 *} |
|
542 |
|
543 text {* |
|
544 \begin{center} |
|
545 \begin{tabular}{@ {}p{3cm}p{3cm}@ {}} |
|
546 @{thm[mode=Rule] |
|
547 Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]} |
|
548 & |
|
549 @{thm[mode=Rule] |
|
550 Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]} |
|
551 \end{tabular} |
|
552 \end{center} |
|
553 |
|
554 |
541 *} |
555 *} |
542 |
556 |
543 section {* Abacus Machines *} |
557 section {* Abacus Machines *} |
544 |
558 |
545 text {* |
559 text {* |