6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
theory Paper
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
3 |
imports "../thys/uncomputable"
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
6 |
(*
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
7 |
hide_const (open) s
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
*)
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
9 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
hide_const (open) Divides.adjust
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
abbreviation
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
"update2 p a \<equiv> update a p"
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
consts DUMMY::'a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
notation (latex output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
Cons ("_::_" [78,77] 73) and
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
set ("") and
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
update2 ("update") and
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
tm_wf0 ("wf") and
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
(*is_even ("iseven") and*)
|
92
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
tcopy_begin ("copy\<^bsub>begin\<^esub>") and
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
tcopy_loop ("copy\<^bsub>loop\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
tcopy_end ("copy\<^bsub>end\<^esub>") and
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
step0 ("step") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
steps0 ("steps") and
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
exponent ("_\<^bsup>_\<^esup>") and
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
(* abc_lm_v ("lookup") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
abc_lm_s ("set") and*)
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
33 |
haltP ("stdhalt") and
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
tcopy ("copy") and
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
35 |
tape_of ("\<langle>_\<rangle>") and
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
36 |
tm_comp ("_ \<oplus> _") and
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>")
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
declare [[show_question_marks = false]]
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
41 |
(* THEOREMS *)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
notation (Rule output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
"==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
syntax (Rule output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
46 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
("\<^raw:\mbox{>_\<^raw:}\\>/ _")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
notation (Axiom output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
55 |
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
56 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
57 |
notation (IfThen output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
59 |
syntax (IfThen output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
notation (IfThenNoBox output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
syntax (IfThenNoBox output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
71 |
"_asm" :: "prop \<Rightarrow> asms" ("_")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
72 |
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
73 |
lemma nats2tape:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
74 |
shows "<([]::nat list)> = []"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
and "<[n]> = Oc \<up> (n + 1)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
76 |
and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
77 |
apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
78 |
apply(case_tac ns)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
79 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
80 |
done
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
81 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
(*>*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
section {* Introduction *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
85 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
88 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
89 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
%\noindent
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
%We formalised in earlier work the correctness proofs for two
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
%algorithms in Isabelle/HOL---one about type-checking in
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
%LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
94 |
%in access control~\cite{WuZhangUrban12}. The formalisations
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
95 |
%uncovered a gap in the informal correctness proof of the former and
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
%made us realise that important details were left out in the informal
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
%model for the latter. However, in both cases we were unable to
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
%formalise in Isabelle/HOL computability arguments about the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
%algorithms.
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
100 |
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
101 |
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
\noindent
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
Suppose you want to mechanise a proof for whether a predicate @{term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
104 |
P}, say, is decidable or not. Decidability of @{text P} usually
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
105 |
amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
106 |
does \emph{not} work in Isabelle/HOL and other HOL theorem provers,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
107 |
since they are based on classical logic where the law of excluded
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
matter whether @{text P} is constructed by computable means. We hit on
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
110 |
this limitation previously when we mechanised the correctness proofs
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
111 |
of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
112 |
were unable to formalise arguments about decidability.
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
113 |
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
114 |
%The same problem would arise if we had formulated
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
115 |
%the algorithms as recursive functions, because internally in
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
116 |
%Isabelle/HOL, like in all HOL-based theorem provers, functions are
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
117 |
%represented as inductively defined predicates too.
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
118 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
119 |
The only satisfying way out of this problem in a theorem prover based
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
120 |
on classical logic is to formalise a theory of computability. Norrish
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
121 |
provided such a formalisation for the HOL. He choose
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
the $\lambda$-calculus as the starting point for his formalisation of
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
123 |
computability theory, because of its ``simplicity'' \cite[Page
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
124 |
297]{Norrish11}. Part of his formalisation is a clever infrastructure
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
125 |
for reducing $\lambda$-terms. He also established the computational
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
126 |
equivalence between the $\lambda$-calculus and recursive functions.
|
52
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
127 |
Nevertheless he concluded that it would be appealing
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
128 |
to have formalisations for more operational models of
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
129 |
computations, such as Turing machines or register machines. One
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
130 |
reason is that many proofs in the literature use them. He noted
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
131 |
however that \cite[Page 310]{Norrish11}:
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
132 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
133 |
\begin{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
134 |
\it``If register machines are unappealing because of their
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
135 |
general fiddliness,\\ Turing machines are an even more
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
136 |
daunting prospect.''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
137 |
\end{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
139 |
\noindent
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
140 |
In this paper we take on this daunting prospect and provide a
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
formalisation of Turing machines, as well as abacus machines (a kind
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
142 |
of register machines) and recursive functions. To see the difficulties
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
143 |
involved with this work, one has to understand that Turing machine
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
144 |
programs can be completely \emph{unstructured}, behaving similar to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
Basic programs involving the infamous goto \cite{Dijkstra68}. This
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
146 |
precludes in the general case a compositional Hoare-style reasoning
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
about Turing programs. We provide such Hoare-rules for when it
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
148 |
\emph{is} possible to reason in a compositional manner (which is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
149 |
fortunately quite often), but also tackle the more complicated case
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
150 |
when we translate abacus programs into Turing programs. This
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
151 |
reasoning about concrete Turing machine programs is usually
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
152 |
left out in the informal literature, e.g.~\cite{Boolos87}.
|
12
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
153 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
154 |
%To see the difficulties
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
155 |
%involved with this work, one has to understand that interactive
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
156 |
%theorem provers, like Isabelle/HOL, are at their best when the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
157 |
%data-structures at hand are ``structurally'' defined, like lists,
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
158 |
%natural numbers, regular expressions, etc. Such data-structures come
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
159 |
%with convenient reasoning infrastructures (for example induction
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
160 |
%principles, recursion combinators and so on). But this is \emph{not}
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
161 |
%the case with Turing machines (and also not with register machines):
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
162 |
%underlying their definitions are sets of states together with
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
%transition functions, all of which are not structurally defined. This
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
164 |
%means we have to implement our own reasoning infrastructure in order
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
165 |
%to prove properties about them. This leads to annoyingly fiddly
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
166 |
%formalisations. We noticed first the difference between both,
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
167 |
%structural and non-structural, ``worlds'' when formalising the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
168 |
%Myhill-Nerode theorem, where regular expressions fared much better
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
%than automata \cite{WuZhangUrban11}. However, with Turing machines
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
170 |
%there seems to be no alternative if one wants to formalise the great
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
171 |
%many proofs from the literature that use them. We will analyse one
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
172 |
%example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
%standard proof of this property uses the notion of universal
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
174 |
%Turing machines.
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
175 |
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
176 |
We are not the first who formalised Turing machines: we are aware
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
177 |
of the preliminary work by Asperti and Ricciotti
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
178 |
\cite{AspertiRicciotti12}. They describe a complete formalisation of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
179 |
Turing machines in the Matita theorem prover, including a universal
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
180 |
Turing machine. However, they do \emph{not} formalise the undecidability of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
181 |
halting problem since their main focus is complexity, rather than
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
182 |
computability theory. They also report that the informal proofs from which they
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
183 |
started are not ``sufficiently accurate to be directly usable as a
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
184 |
guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
185 |
our formalisation we follow mainly the proofs from the textbook
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
186 |
\cite{Boolos87} and found that the description there is quite
|
88
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
187 |
detailed. Some details are left out however: for example, constructing
|
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
188 |
the \emph{copy Turing program} is left as an excerise to the reader; also
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
189 |
\cite{Boolos87} only shows how the universal Turing machine is constructed for Turing
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
190 |
machines computing unary functions. We had to figure out a way to
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
191 |
generalise this result to $n$-ary functions. Similarly, when compiling
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
192 |
recursive functions to abacus machines, the textbook again only shows
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
193 |
how it can be done for 2- and 3-ary functions, but in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
194 |
formalisation we need arbitrary functions. But the general ideas for
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
195 |
how to do this are clear enough in \cite{Boolos87}.
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
%However, one
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
197 |
%aspect that is completely left out from the informal description in
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
198 |
%\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
199 |
%machines are correct. We will introduce Hoare-style proof rules
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
200 |
%which help us with such correctness arguments of Turing machines.
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
201 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
202 |
The main difference between our formalisation and the one by Asperti
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
203 |
and Ricciotti is that their universal Turing machine uses a different
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
204 |
alphabet than the machines it simulates. They write \cite[Page
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
205 |
23]{AspertiRicciotti12}:
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
206 |
|
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
207 |
\begin{quote}\it
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
208 |
``In particular, the fact that the universal machine operates with a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
209 |
different alphabet with respect to the machines it simulates is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
210 |
annoying.''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
211 |
\end{quote}
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
212 |
|
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
213 |
\noindent
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
214 |
In this paper we follow the approach by Boolos et al \cite{Boolos87},
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
215 |
which goes back to Post \cite{Post36}, where all Turing machines
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
216 |
operate on tapes that contain only \emph{blank} or \emph{occupied} cells.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
217 |
Traditionally the content of a cell can be any
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
218 |
character from a finite alphabet. Although computationally equivalent,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
219 |
the more restrictive notion of Turing machines in \cite{Boolos87} makes
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
220 |
the reasoning more uniform. In addition some proofs \emph{about} Turing
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
221 |
machines are simpler. The reason is that one often needs to encode
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
222 |
Turing machines---consequently if the Turing machines are simpler, then the coding
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
223 |
functions are simpler too. Unfortunately, the restrictiveness also makes
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
224 |
it harder to design programs for these Turing machines. In order
|
38
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
225 |
to construct a universal Turing machine we therefore do not follow
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
226 |
\cite{AspertiRicciotti12}, instead follow the proof in
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
227 |
\cite{Boolos87} by translating abacus machines to Turing machines and in
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
228 |
turn recursive functions to abacus machines. The universal Turing
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
229 |
machine can then be constructed as a recursive function.
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
230 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
231 |
\smallskip
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
232 |
\noindent
|
38
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
233 |
{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
234 |
description of Boolos et al \cite{Boolos87} where tapes only have blank or
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
235 |
occupied cells. We mechanise the undecidability of the halting problem and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
236 |
prove the correctness of concrete Turing machines that are needed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
237 |
in this proof; such correctness proofs are left out in the informal literature.
|
72
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
238 |
For reasoning about Turing machine programs we derive Hoare-rules.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
239 |
We also construct the universal Turing machine from \cite{Boolos87} by
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
240 |
translating recursive functions to abacus machines and abacus machines to
|
38
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
241 |
Turing machines. Since we have set up in Isabelle/HOL a very general computability
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
242 |
model and undecidability result, we are able to formalise other
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
243 |
results: we describe a proof of the computational equivalence
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
244 |
of single-sided Turing machines, which is not given in \cite{Boolos87},
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
245 |
but needed for example for formalising the undecidability proof of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
246 |
Wang's tiling problem \cite{Robinson71}.
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
247 |
%We are not aware of any other
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
248 |
%formalisation of a substantial undecidability problem.
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
249 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
250 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
251 |
section {* Turing Machines *}
|
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
252 |
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
253 |
text {* \noindent
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
254 |
Turing machines can be thought of as having a \emph{head},
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
255 |
``gliding'' over a potentially infinite tape. Boolos et
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
256 |
al~\cite{Boolos87} only consider tapes with cells being either blank
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
257 |
or occupied, which we represent by a datatype having two
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
258 |
constructors, namely @{text Bk} and @{text Oc}. One way to
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
259 |
represent such tapes is to use a pair of lists, written @{term "(l,
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
260 |
r)"}, where @{term l} stands for the tape on the left-hand side of
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
261 |
the head and @{term r} for the tape on the right-hand side. We use
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
262 |
the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
|
88
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
263 |
composed of @{term n} elements of @{term Bk}s. We also have the
|
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
264 |
convention that the head, abbreviated @{term hd}, of the right list
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
265 |
is the cell on which the head of the Turing machine currently
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
266 |
scannes. This can be pictured as follows:
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
267 |
%
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
268 |
\begin{center}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
269 |
\begin{tikzpicture}[scale=0.9]
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
270 |
\draw[very thick] (-3.0,0) -- ( 3.0,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
271 |
\draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
272 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
273 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
274 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
275 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
276 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
277 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
278 |
\draw[very thick] (-1.75,0) -- (-1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
279 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
280 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
281 |
\draw[fill] (1.35,0.1) rectangle (1.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
282 |
\draw[fill] (0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
283 |
\draw[fill] (-0.35,0.1) rectangle (-0.65,0.4);
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
284 |
\draw[fill] (-1.65,0.1) rectangle (-1.35,0.4);
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
285 |
\draw (-0.25,0.8) -- (-0.25,-0.8);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
286 |
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
287 |
\node [anchor=base] at (-0.85,-0.5) {\small left list};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
288 |
\node [anchor=base] at (0.40,-0.5) {\small right list};
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
289 |
\node [anchor=base] at (0.1,0.7) {\small head};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
290 |
\node [anchor=base] at (-2.2,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
291 |
\node [anchor=base] at ( 2.3,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
292 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
293 |
\end{center}
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
294 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
295 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
296 |
Note that by using lists each side of the tape is only finite. The
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
297 |
potential infinity is achieved by adding an appropriate blank or occupied cell
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
298 |
whenever the head goes over the ``edge'' of the tape. To
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
299 |
make this formal we define five possible \emph{actions}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
300 |
the Turing machine can perform:
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
301 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
302 |
\begin{center}
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
303 |
\begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
304 |
@{text "a"} & $::=$ & @{term "W0"} & (write blank, @{term Bk})\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
305 |
& $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
306 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
307 |
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
308 |
& $\mid$ & @{term L} & (move left)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
309 |
& $\mid$ & @{term R} & (move right)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
310 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
311 |
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
312 |
& $\mid$ & @{term Nop} & (do-nothing operation)\\
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
313 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
314 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
315 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
316 |
\noindent
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
317 |
We slightly deviate
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
318 |
from the presentation in \cite{Boolos87} and \cite{AspertiRicciotti12}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
319 |
by using the @{term Nop} operation; however its use
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
320 |
will become important when we formalise halting computations and also universal Turing
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
321 |
machines. Given a tape and an action, we can define the
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
322 |
following tape updating function:
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
323 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
324 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
325 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
326 |
@{thm (lhs) update.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
327 |
@{thm (lhs) update.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(2)}\\
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
328 |
@{thm (lhs) update.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(3)}\\
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
329 |
@{thm (lhs) update.simps(4)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(4)}\\
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
330 |
@{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(5)}\\
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
331 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
332 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
333 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
334 |
\noindent
|
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
335 |
The first two clauses replace the head of the right list
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
336 |
with a new @{term Bk} or @{term Oc}, respectively. To see that
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
337 |
these two clauses make sense in case where @{text r} is the empty
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
338 |
list, one has to know that the tail function, @{term tl}, is defined
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
339 |
such that @{term "tl [] == []"} holds. The third clause
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
340 |
implements the move of the head one step to the left: we need
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
341 |
to test if the left-list @{term l} is empty; if yes, then we just prepend a
|
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
342 |
blank cell to the right list; otherwise we have to remove the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
343 |
head from the left-list and prepend it to the right list. Similarly
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
344 |
in the fourth clause for a right move action. The @{term Nop} operation
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
345 |
leaves the the tape unchanged.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
346 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
347 |
%Note that our treatment of the tape is rather ``unsymmetric''---we
|
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
348 |
%have the convention that the head of the right list is where the
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
%head is currently positioned. Asperti and Ricciotti
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
350 |
%\cite{AspertiRicciotti12} also considered such a representation, but
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
351 |
%dismiss it as it complicates their definition for \emph{tape
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
352 |
%equality}. The reason is that moving the head one step to
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
353 |
%the left and then back to the right might change the tape (in case
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
354 |
%of going over the ``edge''). Therefore they distinguish four types
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
355 |
%of tapes: one where the tape is empty; another where the head
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
356 |
%is on the left edge, respectively right edge, and in the middle
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
357 |
%of the tape. The reading, writing and moving of the tape is then
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
358 |
%defined in terms of these four cases. In this way they can keep the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
359 |
%tape in a ``normalised'' form, and thus making a left-move followed
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
360 |
%by a right-move being the identity on tapes. Since we are not using
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
361 |
%the notion of tape equality, we can get away with the unsymmetric
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
362 |
%definition above, and by using the @{term update} function
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
363 |
%cover uniformly all cases including corner cases.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
364 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
365 |
Next we need to define the \emph{states} of a Turing machine.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
366 |
%Given
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
367 |
%how little is usually said about how to represent them in informal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
368 |
%presentations, it might be surprising that in a theorem prover we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
369 |
%have to select carefully a representation. If we use the naive
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
370 |
%representation where a Turing machine consists of a finite set of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
371 |
%states, then we will have difficulties composing two Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
372 |
%machines: we would need to combine two finite sets of states,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
373 |
%possibly renaming states apart whenever both machines share
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
374 |
%states.\footnote{The usual disjoint union operation in Isabelle/HOL
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
375 |
%cannot be used as it does not preserve types.} This renaming can be
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
376 |
%quite cumbersome to reason about.
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
377 |
We follow the choice made in \cite{AspertiRicciotti12}
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
378 |
by representing a state with a natural number and the states in a Turing
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
379 |
machine program by the initial segment of natural numbers starting from @{text 0}.
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
380 |
In doing so we can compose two Turing machine programs by
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
381 |
shifting the states of one by an appropriate amount to a higher
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
382 |
segment and adjusting some ``next states'' in the other.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
383 |
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
384 |
An \emph{instruction} of a Turing machine is a pair consisting of
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
385 |
an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
386 |
machine is then a list of such pairs. Using as an example the following Turing machine
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
387 |
program, which consists of four instructions
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
388 |
%
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
389 |
\begin{equation}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
390 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
391 |
\node [anchor=base] at (0,0) {@{thm dither_def}};
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
392 |
\node [anchor=west] at (-1.5,-0.64)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
393 |
{$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
394 |
= starting state\end{tabular}}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
395 |
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
396 |
\node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
397 |
\node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
398 |
\node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
399 |
\end{tikzpicture}
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
400 |
\label{dither}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
401 |
\end{equation}
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
402 |
%
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
403 |
\noindent
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
404 |
the reader can see we have organised our Turing machine programs so
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
405 |
that segments of two belong to a state. The first component of such a
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
406 |
segment determines what action should be taken and which next state
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
407 |
should be transitioned to in case the head reads a @{term Bk};
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
408 |
similarly the second component determines what should be done in
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
409 |
case of reading @{term Oc}. We have the convention that the first
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
410 |
state is always the \emph{starting state} of the Turing machine.
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
411 |
The @{text 0}-state is special in that it will be used as the
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
412 |
``halting state''. There are no instructions for the @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
413 |
0}-state, but it will always perform a @{term Nop}-operation and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
414 |
remain in the @{text 0}-state. Unlike Asperti and Riccioti
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
415 |
\cite{AspertiRicciotti12}, we have chosen a very concrete
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
416 |
representation for programs, because when constructing a universal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
417 |
Turing machine, we need to define a coding function for programs.
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
418 |
This can be directly done for our programs-as-lists, but is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
419 |
slightly more difficult for the functions used by Asperti and Ricciotti.
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
420 |
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
421 |
Given a program @{term p}, a state
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
422 |
and the cell being read by the head, we need to fetch
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
423 |
the corresponding instruction from the program. For this we define
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
424 |
the function @{term fetch}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
425 |
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
426 |
\begin{equation}\label{fetch}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
427 |
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
428 |
\multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
429 |
@{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
430 |
\multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
431 |
@{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
432 |
\multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
433 |
\end{tabular}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
434 |
\end{equation}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
435 |
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
436 |
\noindent
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
437 |
In this definition the function @{term nth_of} returns the @{text n}th element
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
438 |
from a list, provided it exists (@{term Some}-case), or if it does not, it
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
439 |
returns the default action @{term Nop} and the default state @{text 0}
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
440 |
(@{term None}-case). We often need to restrict Turing machine programs
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
441 |
to be well-formed: a program @{term p} is \emph{well-formed} if it
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
442 |
satisfies the following three properties:
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
443 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
444 |
\begin{center}
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
445 |
@{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]}
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
446 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
447 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
448 |
\noindent
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
449 |
The first states that @{text p} must have at least an instruction for the starting
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
450 |
state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
451 |
state, and the third that every next-state is one of the states mentioned in
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
452 |
the program or being the @{text 0}-state.
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
453 |
|
72
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
454 |
We need to be able to sequentially compose Turing machine programs. Given our
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
455 |
concrete representation, this is relatively straightforward, if
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
456 |
slightly fiddly. We use the following two auxiliary functions:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
457 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
458 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
459 |
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
460 |
@{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
461 |
@{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
462 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
463 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
464 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
465 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
466 |
The first adds @{text n} to all states, exept the @{text 0}-state,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
467 |
thus moving all ``regular'' states to the segment starting at @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
468 |
n}; the second adds @{term "Suc(length p div 2)"} to the @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
469 |
0}-state, thus redirecting all references to the ``halting state''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
470 |
to the first state after the program @{text p}. With these two
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
471 |
functions in place, we can define the \emph{sequential composition}
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
472 |
of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as
|
72
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
473 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
474 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
475 |
@{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
476 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
477 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
478 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
479 |
%This means @{text "p\<^isub>1"} is executed first. Whenever it originally
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
480 |
%transitioned to the @{text 0}-state, it will in the composed program transition to the starting
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
481 |
%state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
482 |
%have been shifted in order to make sure that the states of the composed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
483 |
%program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
484 |
%an initial segment of the natural numbers.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
485 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
486 |
A \emph{configuration} @{term c} of a Turing machine is a state
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
487 |
together with a tape. This is written as @{text "(s, (l, r))"}. We
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
488 |
say a configuration \emph{is final} if @{term "s = (0::nat)"} and we
|
72
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
489 |
say a predicate @{text P} \emph{holds for} a configuration if @{text
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
490 |
"P"} holds for the tape @{text "(l, r)"}. If we have a configuration and a program, we can
|
72
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
491 |
calculate what the next configuration is by fetching the appropriate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
492 |
action and next state from the program, and by updating the state
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
493 |
and tape accordingly. This single step of execution is defined as
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
494 |
the function @{term step}
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
495 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
496 |
\begin{center}
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
497 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
498 |
@{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
499 |
& & @{text "in (s', update (l, r) a)"}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
500 |
\end{tabular}
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
501 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
502 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
503 |
\noindent
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
504 |
where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
505 |
empty it returns @{term Bk}.
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
506 |
It is impossible in Isabelle/HOL to lift the @{term step}-function to realise
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
507 |
a general evaluation function for Turing machines. The reason is that functions in HOL-based
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
508 |
provers need to be terminating, and clearly there are Turing machine
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
509 |
programs that are not. We can however define an evaluation
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
510 |
function that performs exactly @{text n} steps:
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
511 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
512 |
\begin{center}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
513 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
514 |
@{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
515 |
@{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
516 |
\end{tabular}
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
517 |
\end{center}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
518 |
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
519 |
\noindent Recall our definition of @{term fetch} (shown in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
520 |
\eqref{fetch}) with the default value for the @{text 0}-state. In
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
521 |
case a Turing program takes according to the usual textbook
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
522 |
definition \cite{Boolos87} less than @{text n} steps before it
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
523 |
halts, then in our setting the @{term steps}-evaluation does not
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
524 |
actually halt, but rather transitions to the @{text 0}-state (the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
525 |
final state) and remains there performing @{text Nop}-actions until
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
526 |
@{text n} is reached.
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
527 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
528 |
\begin{figure}[t]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
529 |
\begin{center}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
530 |
\begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
531 |
\begin{tabular}[t]{@ {}l@ {}}
|
92
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
532 |
@{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
533 |
\hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
534 |
\hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
535 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
536 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
537 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
538 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
539 |
@{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
540 |
\hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
541 |
\hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Bk\<^esub>, 2), (R, 3), (R, 4),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
542 |
\hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Oc\<^esub>, 5), (R, 4), (L, 6),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
543 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
544 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
545 |
&
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
546 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
547 |
@{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
548 |
\hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>Oc\<^esub>, 3),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
549 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
550 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>Bk\<^esub>, 4), (R, 0),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
551 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
552 |
\end{tabular}
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
553 |
\end{tabular}\\[2mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
554 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
555 |
\begin{tikzpicture}[scale=0.7]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
556 |
\node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
557 |
\node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
558 |
\node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
|
88
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
559 |
\node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_init"}}^{}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
560 |
\node [anchor=base] at (5.6,-0.6) {\small$\overbrace{@{term "tcopy_loop"}}^{}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
561 |
\node [anchor=base] at (10.5,-0.6) {\small$\overbrace{@{term "tcopy_end"}}^{}$};
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
562 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
563 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
564 |
\begin{scope}[shift={(0.5,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
565 |
\draw[very thick] (-0.25,0) -- ( 1.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
566 |
\draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
567 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
568 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
569 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
570 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
571 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
572 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
573 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
574 |
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
575 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
576 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
577 |
\begin{scope}[shift={(2.9,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
578 |
\draw[very thick] (-0.25,0) -- ( 2.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
579 |
\draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
580 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
581 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
582 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
583 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
584 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
585 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
586 |
\draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
587 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
588 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
589 |
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
590 |
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
591 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
592 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
593 |
\begin{scope}[shift={(6.8,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
594 |
\draw[very thick] (-0.75,0) -- ( 3.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
595 |
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
596 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
597 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
598 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
599 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
600 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
601 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
602 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
603 |
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
604 |
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
605 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
606 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
607 |
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
608 |
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
609 |
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
610 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
611 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
612 |
\begin{scope}[shift={(11.7,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
613 |
\draw[very thick] (-0.75,0) -- ( 3.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
614 |
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
615 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
616 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
617 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
618 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
619 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
620 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
621 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
622 |
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
623 |
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
624 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
625 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
626 |
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
627 |
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
628 |
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
629 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
630 |
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
631 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
632 |
\end{tikzpicture}\\[-8mm]\mbox{}
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
633 |
\end{center}
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
634 |
\caption{The components of the \emph{copy Turing machine} (above). If started
|
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
635 |
with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
636 |
the end of the right tape; the second then ``moves'' all @{term Oc}s except the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
637 |
first from the beginning of the tape to the end; the third ``refills'' the original
|
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
638 |
block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
639 |
\label{copy}
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
640 |
\end{figure}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
641 |
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
642 |
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
643 |
We often need to restrict tapes to be in \emph{standard form}, which means
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
644 |
the left list of the tape is either empty or only contains @{text "Bk"}s, and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
645 |
the right list contains some ``clusters'' of @{text "Oc"}s separted by single
|
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
646 |
blanks. To make this formal we define the following function
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
647 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
648 |
\begin{center}
|
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
649 |
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
650 |
@{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
651 |
@{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
652 |
@{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
|
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
653 |
\end{tabular}
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
654 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
655 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
656 |
\noindent
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
657 |
A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l}
|
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
658 |
and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
659 |
leftmost @{term "Oc"} on the tape. Note also that @{text 0} is represented by
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
660 |
a single filled cell, @{text 1} by two filled cells and so on.
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
661 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
662 |
Before we can prove the undecidability of the halting problem for our
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
663 |
Turing machines, we need to analyse two concrete Turing machine
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
664 |
programs and establish that they are correct---that means they are
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
665 |
``doing what they are supposed to be doing''. Such correctness proofs are usually left
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
666 |
out in the informal literature, for example \cite{Boolos87}. One program
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
667 |
we need to prove correct is the @{term dither} program shown in \eqref{dither}
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
668 |
and the other program is @{term "tcopy"} defined as
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
669 |
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
670 |
\begin{equation}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
671 |
\mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
672 |
@{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
673 |
\end{tabular}}\label{tcopy}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
674 |
\end{equation}
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
675 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
676 |
\noindent
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
677 |
whose three components are given in Figure~\ref{copy}. To the prove
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
678 |
correctness of these Turing machine programs, we introduce the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
679 |
notion of total correctness defined in terms of
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
680 |
\emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
681 |
to the notion of \emph{realisability} in \cite{AspertiRicciotti12}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
682 |
They implement the
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
683 |
idea that a program @{term p} started in state @{term "1::nat"} with
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
684 |
a tape satisfying @{term P} will after some @{text n} steps halt (have
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
685 |
transitioned into the halting state) with a tape satisfying @{term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
686 |
Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
687 |
realising the case that a program @{term p} started with a tape
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
688 |
satisfying @{term P} will loop (never transition into the halting
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
689 |
state). Both notion are formally defined as
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
690 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
691 |
\begin{center}
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
692 |
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
693 |
\begin{tabular}[t]{@ {}l@ {}}
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
694 |
\colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
695 |
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
696 |
\hspace{7mm}if @{term "P (l, r)"} holds then\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
697 |
\hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
698 |
\hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
699 |
\hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
700 |
\end{tabular} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
701 |
\begin{tabular}[t]{@ {}l@ {}}
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
702 |
\colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
703 |
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
704 |
\hspace{7mm}if @{term "P (l, r)"} holds then\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
705 |
\hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
706 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
707 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
708 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
709 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
710 |
\noindent
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
711 |
Like Asperti and Ricciotti with their notion of realisability, we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
712 |
have set up our Hoare-style reasoning so that we can deal explicitly
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
713 |
with total correctness and non-terminantion, rather than have
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
714 |
notions for partial correctness and termination. Although the latter
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
715 |
would allow us to reason more uniformly (only using Hoare-triples),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
716 |
we prefer our definitions because we can derive (below) simple
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
717 |
Hoare-rules for sequentially composed Turing programs. In this way
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
718 |
we can reason about the correctness of @{term "tcopy_init"}, for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
719 |
example, completely separately from @{term "tcopy_loop"} and @{term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
720 |
"tcopy_end"}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
721 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
722 |
It is realatively straightforward to prove that the Turing program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
723 |
@{term "dither"} shown in \eqref{dither} is correct. This program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
724 |
should be the ``identity'' when started with a standard tape representing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
725 |
@{text "1"} but loop when started with @{text 0} instead.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
726 |
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
727 |
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
728 |
\begin{center}
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
729 |
\begin{tabular}{l@ {\hspace{3mm}}lcl}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
730 |
& \multicolumn{1}{c}{start tape}\\[1mm]
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
731 |
\raisebox{2mm}{halting case:} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
732 |
\begin{tikzpicture}[scale=0.8]
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
733 |
\draw[very thick] (-2,0) -- ( 0.75,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
734 |
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
735 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
736 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
737 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
738 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
739 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
740 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
741 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
742 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
743 |
\node [anchor=base] at (-1.7,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
744 |
\end{tikzpicture}
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
745 |
& \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
746 |
\begin{tikzpicture}[scale=0.8]
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
747 |
\draw[very thick] (-2,0) -- ( 0.75,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
748 |
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
749 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
750 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
751 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
752 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
753 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
754 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
755 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
756 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
757 |
\node [anchor=base] at (-1.7,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
758 |
\end{tikzpicture}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
759 |
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
760 |
\raisebox{2mm}{non-halting case:} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
761 |
\begin{tikzpicture}[scale=0.8]
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
762 |
\draw[very thick] (-2,0) -- ( 0.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
763 |
\draw[very thick] (-2,0.5) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
764 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
765 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
766 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
767 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
768 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
769 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
770 |
\node [anchor=base] at (-1.7,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
771 |
\end{tikzpicture}
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
772 |
& \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
773 |
\raisebox{2mm}{loops}
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
774 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
775 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
776 |
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
777 |
\noindent
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
778 |
We can prove the following Hoare-statements:
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
779 |
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
780 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
781 |
\begin{tabular}{l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
782 |
@{thm dither_halts}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
783 |
@{thm dither_loops}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
784 |
\end{tabular}
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
785 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
786 |
|
77
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
787 |
\noindent
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
788 |
The first is by a simple calculation. The second is by induction on the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
789 |
number of steps we can perform starting from the input tape.
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
790 |
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
791 |
The purpose of the @{term tcopy} program defined in \eqref{tcopy} is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
792 |
to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
793 |
started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
794 |
a value on the tape. Reasoning about this program is substantially
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
795 |
harder than about @{term dither}. To ease the burden, we can prove
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
796 |
the following Hoare-rules for sequentially composed programs.
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
797 |
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
798 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
799 |
\begin{tabular}{@ {}p{3cm}@ {\hspace{9mm}}p{3cm}@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
800 |
@{thm[mode=Rule]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
801 |
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"]}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
802 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
803 |
@{thm[mode=Rule]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
804 |
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"]}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
805 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
806 |
\end{center}
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
807 |
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
808 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
809 |
The first corresponds to the usual Hoare-rule for composition of imperative
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
810 |
programs, where @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
811 |
all tapes @{term "(l, r)"}. The second rule covers the case where rughly the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
812 |
first program terminates generating a tape for which the second program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
813 |
loops. These are two cases we need in our proof for undecidability.
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
814 |
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
815 |
The Hoare-rules above allow us to prove the correctness of @{term tcopy}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
816 |
by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
817 |
and @{term "tcopy_end"} in isolation. We will show some details for the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
818 |
the program @{term "tcopy_begin"}.
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
819 |
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
820 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
821 |
assertion holds for all tapes
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
822 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
823 |
Hoare rule for composition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
824 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
825 |
For showing the undecidability of the halting problem, we need to consider
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
826 |
two specific Turing machines. copying TM and dithering TM
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
827 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
828 |
correctness of the copying TM
|
19
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
829 |
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
830 |
measure for the copying TM, which we however omit.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
831 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
832 |
halting problem
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
833 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
834 |
Magnus: invariants -- Section 5.4.5 on page 75.
|
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
835 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
836 |
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
837 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
838 |
section {* Abacus Machines *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
839 |
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
840 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
841 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
842 |
Boolos et al \cite{Boolos87} use abacus machines as a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
843 |
stepping stone for making it less laborious to write
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
844 |
programs for Turing machines. Abacus machines operate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
845 |
over an unlimited number of registers $R_0$, $R_1$, \ldots
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
846 |
each being able to hold an arbitrary large natural number.
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
847 |
We use natural numbers to refer to registers, but also
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
848 |
to refer to \emph{opcodes} of abacus
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
849 |
machines. Obcodes are given by the datatype
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
850 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
851 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
852 |
\begin{tabular}{rcll}
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
853 |
@{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
854 |
& $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
855 |
& & & then decrement it by one\\
|
26
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
856 |
& & & otherwise jump to opcode $o$\\
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
857 |
& $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
858 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
859 |
\end{center}
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
860 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
861 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
862 |
A \emph{program} of an abacus machine is a list of such
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
863 |
obcodes. For example the program clearing the register
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
864 |
$R$ (setting it to 0) can be defined as follows:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
865 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
866 |
\begin{center}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
867 |
%@ {thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
868 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
869 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
870 |
\noindent
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
871 |
The second opcode @{term "Goto 0"} in this program means we
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
872 |
jump back to the first opcode, namely @{text "Dec R o"}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
873 |
The \emph{memory} $m$ of an abacus machine holding the values
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
874 |
of the registers is represented as a list of natural numbers.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
875 |
We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
876 |
which looks up the content of register $R$; if $R$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
877 |
is not in this list, then we return 0. Similarly we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
878 |
have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
879 |
sets the value of $R$ to $n$, and if $R$ was not yet in $m$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
880 |
it pads it approriately with 0s.
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
881 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
882 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
883 |
Abacus machine halts when it jumps out of range.
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
884 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
885 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
886 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
887 |
section {* Recursive Functions *}
|
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
888 |
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
889 |
section {* Wang Tiles\label{Wang} *}
|
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
890 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
891 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
892 |
Used in texture mapings - graphics
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
893 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
894 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
895 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
896 |
section {* Related Work *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
897 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
898 |
text {*
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
899 |
The most closely related work is by Norrish \cite{Norrish11}, and Asperti and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
900 |
Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
901 |
lambda-terms. For this he introduced a clever rewriting technology
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
902 |
based on combinators and de-Bruijn indices for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
903 |
rewriting modulo $\beta$-equivalence (to keep it manageable)
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
904 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
905 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
906 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
907 |
Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
908 |
@{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
909 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
910 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
911 |
\begin{tabular}{l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
912 |
@{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
913 |
\hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
914 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
915 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
916 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
917 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
918 |
where @{text 1} stands for the starting state and @{text 0} for our final state.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
919 |
A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
920 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
921 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
922 |
@{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
923 |
\<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
924 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
925 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
926 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
927 |
Later on we need to consider specific Turing machines that
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
928 |
start with a tape in standard form and halt the computation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
929 |
in standard form. To define a tape in standard form, it is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
930 |
useful to have an operation %@{ term "tape_of_nat_list DUMMY"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
931 |
that translates lists of natural numbers into tapes.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
932 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
933 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
934 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
935 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
936 |
%@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
937 |
%@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
938 |
%@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
939 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
940 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
941 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
942 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
943 |
By this we mean
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
944 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
945 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
946 |
%@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
947 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
948 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
949 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
950 |
This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
951 |
and the head pointing to the first one; the Turing machine
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
952 |
halts with a tape consisting of some @{term Bk}s, followed by a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
953 |
``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
954 |
The head in the output is pointing again at the first @{term Oc}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
955 |
The intuitive meaning of this definition is to start the Turing machine with a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
956 |
tape corresponding to a value @{term n} and producing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
957 |
a new tape corresponding to the value @{term l} (the number of @{term Oc}s
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
958 |
clustered on the output tape).
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
959 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
960 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
961 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
962 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
963 |
(*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
964 |
Questions:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
965 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
966 |
Can this be done: Ackerman function is not primitive
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
967 |
recursive (Nora Szasz)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
968 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
969 |
Tape is represented as two lists (finite - usually infinite tape)?
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
970 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
971 |
*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
972 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
973 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
974 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
975 |
end
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
976 |
(*>*) |