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
|
111
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
3 |
imports "../thys/abacus"
|
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 |
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
hide_const (open) Divides.adjust
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
abbreviation
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
"update2 p a \<equiv> update a p"
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
consts DUMMY::'a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
(* THEOREMS *)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
notation (Rule output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
"==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
syntax (Rule output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
("\<^raw:\mbox{>_\<^raw:}\\>/ _")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
notation (Axiom output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
33 |
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
35 |
notation (IfThen output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
36 |
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
syntax (IfThen output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
"_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
|
41 |
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
notation (IfThenNoBox output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
syntax (IfThenNoBox 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:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
"_asm" :: "prop \<Rightarrow> asms" ("_")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
|
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 |
context uncomputable
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
55 |
notation (latex output)
|
100
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
56 |
Cons ("_::_" [48,47] 48) and
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
57 |
set ("") and
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
59 |
W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
update2 ("update") and
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
tm_wf0 ("wf") and
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
(*is_even ("iseven") and*)
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
tcopy_begin ("cbegin") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
tcopy_loop ("cloop") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
tcopy_end ("cend") and
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
step0 ("step") and
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
tcontra ("contra") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
code_tcontra ("code contra") and
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
steps0 ("steps") and
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
exponent ("_\<^bsup>_\<^esup>") and
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
71 |
haltP ("halts") and
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
72 |
tcopy ("copy") and
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
73 |
tape_of ("\<langle>_\<rangle>") and
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
74 |
tm_comp ("_ \<oplus> _") and
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
76 |
inv_begin0 ("I\<^isub>0") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
77 |
inv_begin1 ("I\<^isub>1") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
78 |
inv_begin2 ("I\<^isub>2") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
79 |
inv_begin3 ("I\<^isub>3") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
80 |
inv_begin4 ("I\<^isub>4") and
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
81 |
inv_begin ("I\<^bsub>cbegin\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
82 |
inv_loop1 ("J\<^isub>1") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
83 |
inv_loop0 ("J\<^isub>0") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
84 |
inv_end1 ("K\<^isub>1") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
85 |
inv_end0 ("K\<^isub>0") and
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
measure_begin_step ("M\<^bsub>cbegin\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
layout_of ("layout") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
88 |
findnth ("find'_nth")
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
lemma inv_begin_print:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
"s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
94 |
"s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
95 |
"s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
"s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
"s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
apply(case_tac [!] tp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
by (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
100 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
101 |
lemma inv1:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
shows "0 < n \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
unfolding assert_imp_def
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
104 |
unfolding inv_loop1.simps inv_begin0.simps
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
105 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
106 |
apply(rule_tac x="1" in exI)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
107 |
apply(auto simp add: replicate.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
110 |
lemma inv2:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
111 |
shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
112 |
apply(rule ext)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
113 |
apply(case_tac x)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
114 |
apply(simp add: inv_end1.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
115 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
116 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
117 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
118 |
lemma measure_begin_print:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
119 |
shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
120 |
"s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
121 |
"s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
"s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
123 |
by (simp_all)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
124 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
125 |
declare [[show_question_marks = false]]
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
126 |
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
127 |
lemma nats2tape:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
128 |
shows "<([]::nat list)> = []"
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
129 |
and "<[n]> = <n>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
130 |
and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
131 |
and "<(n, m)> = <n> @ [Bk] @ <m>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
132 |
and "<[n, m]> = <(n, m)>"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
133 |
and "<n> = Oc \<up> (n + 1)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
134 |
apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
135 |
apply(case_tac ns)
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
136 |
apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
137 |
done
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
139 |
lemmas HR1 =
|
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
140 |
Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
142 |
lemmas HR2 =
|
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
143 |
Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
144 |
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
lemma inv_begin01:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
146 |
assumes "n > 1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
148 |
using assms by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
149 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
150 |
lemma inv_begin02:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
151 |
assumes "n = 1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
152 |
shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
153 |
using assms by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
154 |
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
155 |
|
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
156 |
lemma layout:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
157 |
shows "layout_of [] = []"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
158 |
and "layout_of ((Inc R\<iota>)#os) = (2 * R\<iota> + 9)#(layout_of os)"
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
159 |
and "layout_of ((Dec R\<iota> i)#os) = (2 * R\<iota> + 16)#(layout_of os)"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
160 |
and "layout_of ((Goto i)#os) = 1#(layout_of os)"
|
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
161 |
by(auto simp add: layout_of.simps length_of.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
162 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
164 |
(*>*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
165 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
166 |
section {* Introduction *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
167 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
168 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
170 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
171 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
172 |
%\noindent
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
%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
|
174 |
%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
|
175 |
%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
|
176 |
%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
|
177 |
%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
|
178 |
%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
|
179 |
%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
|
180 |
%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
|
181 |
%algorithms.
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
182 |
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
183 |
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
184 |
\noindent
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
185 |
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
|
186 |
P}, say, is decidable or not. Decidability of @{text P} usually
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
187 |
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
|
188 |
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
|
189 |
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
|
190 |
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
|
191 |
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
|
192 |
this limitation previously when we mechanised the correctness proofs
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
193 |
of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
194 |
were unable to formalise arguments about decidability or undecidability.
|
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 |
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
%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
|
197 |
%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
|
198 |
%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
|
199 |
%represented as inductively defined predicates too.
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
200 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
201 |
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
|
202 |
on classical logic is to formalise a theory of computability. Norrish
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
203 |
provided such a formalisation for HOL4. He choose the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
204 |
$\lambda$-calculus as the starting point for his formalisation because
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
205 |
of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
206 |
formalisation is a clever infrastructure for reducing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
207 |
$\lambda$-terms. He also established the computational equivalence
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
208 |
between the $\lambda$-calculus and recursive functions. Nevertheless
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
209 |
he concluded that it would be appealing to have formalisations for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
210 |
more operational models of computations, such as Turing machines or
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
211 |
register machines. One reason is that many proofs in the literature
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
212 |
use them. He noted however that \cite[Page 310]{Norrish11}:
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
213 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
214 |
\begin{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
215 |
\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
|
216 |
general fiddliness,\\ Turing machines are an even more
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
217 |
daunting prospect.''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
218 |
\end{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
219 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
220 |
\noindent
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
221 |
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
|
222 |
formalisation of Turing machines, as well as abacus machines (a kind
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
223 |
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
|
224 |
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
|
225 |
programs can be completely \emph{unstructured}, behaving similar to
|
116
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
226 |
Basic programs containing the infamous goto-statements \cite{Dijkstra68}. This
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
227 |
precludes in the general case a compositional Hoare-style reasoning
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
228 |
about Turing programs. We provide such Hoare-rules for when it
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
229 |
\emph{is} possible to reason in a compositional manner (which is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
230 |
fortunately quite often), but also tackle the more complicated case
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
231 |
when we translate abacus programs into Turing programs. This
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
232 |
reasoning about concrete Turing machine programs is usually
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
233 |
left out in the informal literature, e.g.~\cite{Boolos87}.
|
12
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
234 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
235 |
%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
|
236 |
%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
|
237 |
%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
|
238 |
%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
|
239 |
%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
|
240 |
%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
|
241 |
%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
|
242 |
%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
|
243 |
%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
|
244 |
%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
|
245 |
%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
|
246 |
%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
|
247 |
%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
|
248 |
%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
|
249 |
%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
|
250 |
%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
|
251 |
%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
|
252 |
%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
|
253 |
%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
|
254 |
%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
|
255 |
%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
|
256 |
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
257 |
We are not the first who formalised Turing machines: we are aware of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
258 |
the work by Asperti and Ricciotti \cite{AspertiRicciotti12}. They
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
259 |
describe a complete formalisation of Turing machines in the Matita
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
260 |
theorem prover, including a universal Turing machine. However, they do
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
261 |
\emph{not} formalise the undecidability of the halting problem since
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
262 |
their main focus is complexity, rather than computability theory. They
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
263 |
also report that the informal proofs from which they started are not
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
264 |
``sufficiently accurate to be directly usable as a guideline for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
265 |
formalization'' \cite[Page 2]{AspertiRicciotti12}. For our
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
266 |
formalisation we follow mainly the proofs from the textbook by Boolos
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
267 |
et al \cite{Boolos87} and found that the description there is quite
|
88
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
268 |
detailed. Some details are left out however: for example, constructing
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
269 |
the \emph{copy Turing machine} is left as an excerise to the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
270 |
reader---a correctness proof is not mentioned at all; also \cite{Boolos87}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
271 |
only shows how the universal Turing machine is constructed for Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
272 |
machines computing unary functions. We had to figure out a way to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
273 |
generalise this result to $n$-ary functions. Similarly, when compiling
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
274 |
recursive functions to abacus machines, the textbook again only shows
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
275 |
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
|
276 |
formalisation we need arbitrary functions. But the general ideas for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
277 |
how to do this are clear enough in \cite{Boolos87}.
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
278 |
%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
|
279 |
%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
|
280 |
%\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
|
281 |
%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
|
282 |
%which help us with such correctness arguments of Turing machines.
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
283 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
284 |
The main difference between our formalisation and the one by Asperti
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
285 |
and Ricciotti is that their universal Turing machine uses a different
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
286 |
alphabet than the machines it simulates. They write \cite[Page
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
287 |
23]{AspertiRicciotti12}:
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
288 |
|
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
289 |
\begin{quote}\it
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
290 |
``In particular, the fact that the universal machine operates with a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
291 |
different alphabet with respect to the machines it simulates is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
292 |
annoying.''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
293 |
\end{quote}
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
294 |
|
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
295 |
\noindent
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
296 |
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
|
297 |
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
|
298 |
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
|
299 |
Traditionally the content of a cell can be any
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
300 |
character from a finite alphabet. Although computationally equivalent,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
301 |
the more restrictive notion of Turing machines in \cite{Boolos87} makes
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
302 |
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
|
303 |
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
|
304 |
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
|
305 |
functions are simpler too. Unfortunately, the restrictiveness also makes
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
306 |
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
|
307 |
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
|
308 |
\cite{AspertiRicciotti12}, instead follow the proof in
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
309 |
\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
|
310 |
turn recursive functions to abacus machines. The universal Turing
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
311 |
machine can then be constructed as a recursive function.
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
312 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
313 |
\smallskip
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
314 |
\noindent
|
38
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
315 |
{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
316 |
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
|
317 |
occupied cells. We mechanise the undecidability of the halting problem and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
318 |
prove the correctness of concrete Turing machines that are needed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
319 |
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
|
320 |
For reasoning about Turing machine programs we derive Hoare-rules.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
321 |
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
|
322 |
translating recursive functions to abacus machines and abacus machines to
|
38
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
323 |
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
|
324 |
model and undecidability result, we are able to formalise other
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
325 |
results: we describe a proof of the computational equivalence
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
326 |
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
|
327 |
but needed for example for formalising the undecidability proof of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
328 |
Wang's tiling problem \cite{Robinson71}.
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
329 |
%We are not aware of any other
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
330 |
%formalisation of a substantial undecidability problem.
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
331 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
332 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
333 |
section {* Turing Machines *}
|
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
334 |
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
335 |
text {* \noindent
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
336 |
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
|
337 |
``gliding'' over a potentially infinite tape. Boolos et
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
338 |
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
|
339 |
or occupied, which we represent by a datatype having two
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
340 |
constructors, namely @{text Bk} and @{text Oc}. One way to
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
341 |
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
|
342 |
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
|
343 |
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
|
344 |
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
|
345 |
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
|
346 |
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
|
347 |
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
|
348 |
scannes. This can be pictured as follows:
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
%
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
350 |
\begin{center}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
351 |
\begin{tikzpicture}[scale=0.9]
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
352 |
\draw[very thick] (-3.0,0) -- ( 3.0,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
353 |
\draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
354 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
355 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
356 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
357 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
358 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
359 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
360 |
\draw[very thick] (-1.75,0) -- (-1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
361 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
362 |
\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
|
363 |
\draw[fill] (1.35,0.1) rectangle (1.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
364 |
\draw[fill] (0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
365 |
\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
|
366 |
\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
|
367 |
\draw (-0.25,0.8) -- (-0.25,-0.8);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
368 |
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
369 |
\node [anchor=base] at (-0.85,-0.5) {\small left list};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
370 |
\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
|
371 |
\node [anchor=base] at (0.1,0.7) {\small head};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
372 |
\node [anchor=base] at (-2.2,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
373 |
\node [anchor=base] at ( 2.3,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
374 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
375 |
\end{center}
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
376 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
377 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
378 |
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
|
379 |
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
|
380 |
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
|
381 |
make this formal we define five possible \emph{actions}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
382 |
the Turing machine can perform:
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
383 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
384 |
\begin{center}
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
385 |
\begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
386 |
@{text "a"} & $::=$ & @{term "W0"} & (write blank, @{term Bk})\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
387 |
& $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
388 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
389 |
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
390 |
& $\mid$ & @{term L} & (move left)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
391 |
& $\mid$ & @{term R} & (move right)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
392 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
393 |
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
394 |
& $\mid$ & @{term Nop} & (do-nothing operation)\\
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
395 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
396 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
397 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
398 |
\noindent
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
399 |
We slightly deviate
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
400 |
from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12})
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
401 |
by using the @{term Nop} operation; however its use
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
402 |
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
|
403 |
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
|
404 |
following tape updating function:
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
405 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
406 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
407 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
408 |
@{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
|
409 |
@{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
|
410 |
@{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
|
411 |
@{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
|
412 |
@{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
|
413 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
414 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
415 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
416 |
\noindent
|
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
417 |
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
|
418 |
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
|
419 |
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
|
420 |
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
|
421 |
such that @{term "tl [] == []"} holds. The third clause
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
422 |
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
|
423 |
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
|
424 |
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
|
425 |
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
|
426 |
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
|
427 |
leaves the the tape unchanged.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
428 |
|
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 |
%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
|
430 |
%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
|
431 |
%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
|
432 |
%\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
|
433 |
%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
|
434 |
%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
|
435 |
%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
|
436 |
%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
|
437 |
%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
|
438 |
%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
|
439 |
%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
|
440 |
%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
|
441 |
%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
|
442 |
%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
|
443 |
%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
|
444 |
%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
|
445 |
%cover uniformly all cases including corner cases.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
446 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
447 |
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
|
448 |
%Given
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
449 |
%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
|
450 |
%presentations, it might be surprising that in a theorem prover we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
451 |
%have to select carefully a representation. If we use the naive
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
452 |
%representation where a Turing machine consists of a finite set of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
453 |
%states, then we will have difficulties composing two Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
454 |
%machines: we would need to combine two finite sets of states,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
455 |
%possibly renaming states apart whenever both machines share
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
456 |
%states.\footnote{The usual disjoint union operation in Isabelle/HOL
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
457 |
%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
|
458 |
%quite cumbersome to reason about.
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
459 |
We follow the choice made in \cite{AspertiRicciotti12}
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
460 |
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
|
461 |
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
|
462 |
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
|
463 |
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
|
464 |
segment and adjusting some ``next states'' in the other.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
465 |
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
466 |
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
|
467 |
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
|
468 |
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
|
469 |
program, which consists of four instructions
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
470 |
%
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
471 |
\begin{equation}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
472 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
473 |
\node [anchor=base] at (0,0) {@{thm dither_def}};
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
474 |
\node [anchor=west] at (-1.5,-0.64)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
475 |
{$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
476 |
= starting state\end{tabular}}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
477 |
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
478 |
\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
|
479 |
\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
|
480 |
\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
|
481 |
\end{tikzpicture}
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
482 |
\label{dither}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
483 |
\end{equation}
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
484 |
%
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
485 |
\noindent
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
486 |
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
|
487 |
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
|
488 |
segment determines what action should be taken and which next state
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
489 |
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
|
490 |
similarly the second component determines what should be done in
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
491 |
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
|
492 |
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
|
493 |
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
|
494 |
``halting state''. There are no instructions for the @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
495 |
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
|
496 |
remain in the @{text 0}-state. Unlike Asperti and Riccioti
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
497 |
\cite{AspertiRicciotti12}, we have chosen a very concrete
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
498 |
representation for programs, because when constructing a universal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
499 |
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
|
500 |
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
|
501 |
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
|
502 |
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
503 |
Given a program @{term p}, a state
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
504 |
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
|
505 |
the corresponding instruction from the program. For this we define
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
506 |
the function @{term fetch}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
507 |
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
508 |
\begin{equation}\label{fetch}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
509 |
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
510 |
\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
|
511 |
@{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
|
512 |
\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
|
513 |
@{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
|
514 |
\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
|
515 |
\end{tabular}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
516 |
\end{equation}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
517 |
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
518 |
\noindent
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
519 |
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
|
520 |
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
|
521 |
returns the default action @{term Nop} and the default state @{text 0}
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
522 |
(@{term None}-case). We often have to restrict Turing machine programs
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
523 |
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
|
524 |
satisfies the following three properties:
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
525 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
526 |
\begin{center}
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
527 |
@{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
|
528 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
529 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
530 |
\noindent
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
531 |
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
|
532 |
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
|
533 |
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
|
534 |
the program or being the @{text 0}-state.
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
535 |
|
72
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
536 |
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
|
537 |
concrete representation, this is relatively straightforward, if
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
538 |
slightly fiddly. We use the following two auxiliary functions:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
539 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
540 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
541 |
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
542 |
@{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
543 |
@{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
|
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 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
546 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
547 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
548 |
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
|
549 |
thus moving all ``regular'' states to the segment starting at @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
550 |
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
|
551 |
0}-state, thus redirecting all references to the ``halting state''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
552 |
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
|
553 |
functions in place, we can define the \emph{sequential composition}
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
554 |
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
|
555 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
556 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
557 |
@{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
|
558 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
559 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
560 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
561 |
%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
|
562 |
%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
|
563 |
%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
|
564 |
%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
|
565 |
%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
|
566 |
%an initial segment of the natural numbers.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
567 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
568 |
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
|
569 |
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
|
570 |
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
|
571 |
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
|
572 |
"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
|
573 |
calculate what the next configuration is by fetching the appropriate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
574 |
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
|
575 |
and tape accordingly. This single step of execution is defined as
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
576 |
the function @{term step}
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
577 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
578 |
\begin{center}
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
579 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
580 |
@{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
|
581 |
& & @{text "in (s', update (l, r) a)"}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
582 |
\end{tabular}
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
583 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
584 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
585 |
\noindent
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
586 |
where @{term "read r"} returns the head of the list @{text r}, or if
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
587 |
@{text r} is empty it returns @{term Bk}. It is impossible in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
588 |
Isabelle/HOL to lift the @{term step}-function in order to realise a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
589 |
general evaluation function for Turing machines programs. The reason
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
590 |
is that functions in HOL-based provers need to be terminating, and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
591 |
clearly there are programs that are not. We can however define a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
592 |
recursive evaluation function that performs exactly @{text n} steps:
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
593 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
594 |
\begin{center}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
595 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
596 |
@{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
|
597 |
@{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
|
598 |
\end{tabular}
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
599 |
\end{center}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
600 |
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
601 |
\noindent Recall our definition of @{term fetch} (shown in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
602 |
\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
|
603 |
case a Turing program takes according to the usual textbook
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
604 |
definition, say \cite{Boolos87}, less than @{text n} steps before it
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
605 |
halts, then in our setting the @{term steps}-evaluation does not
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
606 |
actually halt, but rather transitions to the @{text 0}-state (the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
607 |
final state) and remains there performing @{text Nop}-actions until
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
608 |
@{text n} is reached.
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
609 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
610 |
\begin{figure}[t]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
611 |
\begin{center}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
612 |
\begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
613 |
\begin{tabular}[t]{@ {}l@ {}}
|
92
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
614 |
@{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
615 |
\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
|
616 |
\hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
617 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
618 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
619 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
620 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
621 |
@{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
622 |
\hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
623 |
\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
|
624 |
\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
|
625 |
\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
|
626 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
627 |
&
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
628 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
629 |
@{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
630 |
\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
|
631 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
632 |
\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
|
633 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
634 |
\end{tabular}
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
635 |
\end{tabular}\\[2mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
636 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
637 |
\begin{tikzpicture}[scale=0.7]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
638 |
\node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
639 |
\node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
640 |
\node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
|
98
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
641 |
\node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_begin"}}^{}$};
|
88
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
642 |
\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
|
643 |
\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
|
644 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
645 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
646 |
\begin{scope}[shift={(0.5,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
647 |
\draw[very thick] (-0.25,0) -- ( 1.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
648 |
\draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
649 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
650 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
651 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
652 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
653 |
\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
|
654 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
655 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
656 |
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
657 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
658 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
659 |
\begin{scope}[shift={(2.9,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
660 |
\draw[very thick] (-0.25,0) -- ( 2.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
661 |
\draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
662 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
663 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
664 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
665 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
666 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
667 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
668 |
\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
|
669 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
670 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
671 |
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
672 |
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
673 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
674 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
675 |
\begin{scope}[shift={(6.8,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
676 |
\draw[very thick] (-0.75,0) -- ( 3.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
677 |
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
678 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
679 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
680 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
681 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
682 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
683 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
684 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
685 |
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
686 |
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
687 |
\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
|
688 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
689 |
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
690 |
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
691 |
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
692 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
693 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
694 |
\begin{scope}[shift={(11.7,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
695 |
\draw[very thick] (-0.75,0) -- ( 3.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
696 |
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
697 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
698 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
699 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
700 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
701 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
702 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
703 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
704 |
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
705 |
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
706 |
\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
|
707 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
708 |
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
709 |
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
710 |
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
711 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
712 |
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
713 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
714 |
\end{tikzpicture}\\[-8mm]\mbox{}
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
715 |
\end{center}
|
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
716 |
\caption{The three components of the \emph{copy Turing machine} (above). If started
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
717 |
(below) 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
|
718 |
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
|
719 |
first from the beginning of the tape to the end; the third ``refills'' the original
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
720 |
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
|
721 |
\label{copy}
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
722 |
\end{figure}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
723 |
|
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
724 |
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
725 |
We often need to restrict tapes to be in standard form, which means
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
726 |
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
|
727 |
the right list contains some ``clusters'' of @{text "Oc"}s separted by single
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
728 |
blanks. To make this formal we define the following overloaded function
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
729 |
encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
730 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
731 |
\begin{center}
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
732 |
\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
733 |
@{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
734 |
@{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
735 |
\end{tabular}\hspace{6mm}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
736 |
\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
737 |
@{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
738 |
@{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
739 |
@{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
|
84
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
740 |
\end{tabular}
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
741 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
742 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
743 |
\noindent
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
744 |
A \emph{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
|
745 |
and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
|
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
746 |
leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
747 |
is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
|
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
748 |
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
749 |
Before we can prove the undecidability of the halting problem for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
750 |
our Turing machines working on standard tapes, we have to analyse
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
751 |
two concrete Turing machine programs and establish that they are
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
752 |
correct---that means they are ``doing what they are supposed to be
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
753 |
doing''. Such correctness proofs are usually left out in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
754 |
informal literature, for example \cite{Boolos87}. The first program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
755 |
we need to prove correct is the @{term dither} program shown in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
756 |
\eqref{dither} and the second program is @{term "tcopy"} defined as
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
757 |
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
758 |
\begin{equation}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
759 |
\mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
760 |
@{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
761 |
\end{tabular}}\label{tcopy}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
762 |
\end{equation}
|
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
763 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
764 |
\noindent
|
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
765 |
whose three components are given in Figure~\ref{copy}. For our
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
766 |
correctness proofs, we introduce the notion of total correctness
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
767 |
defined in terms of \emph{Hoare-triples}, written @{term "{P} p
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
768 |
{Q}"}. They implement the idea that a program @{term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
769 |
p} started in state @{term "1::nat"} with a tape satisfying @{term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
770 |
P} will after some @{text n} steps halt (have transitioned into the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
771 |
halting state) with a tape satisfying @{term Q}. This idea is very
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
772 |
similar to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. We
|
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
773 |
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
|
774 |
implementing the case that a program @{term p} started with a tape
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
775 |
satisfying @{term P} will loop (never transition into the halting
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
776 |
state). Both notion are formally defined as
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
777 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
778 |
\begin{center}
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
779 |
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
780 |
\begin{tabular}[t]{@ {}l@ {}}
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
781 |
\colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
782 |
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
783 |
\hspace{7mm}if @{term "P (l, r)"} holds then\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
784 |
\hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
785 |
\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
|
786 |
\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
|
787 |
\end{tabular} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
788 |
\begin{tabular}[t]{@ {}l@ {}}
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
789 |
\colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
790 |
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
791 |
\hspace{7mm}if @{term "P (l, r)"} holds then\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
792 |
\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
|
793 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
794 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
795 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
796 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
797 |
\noindent
|
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
798 |
For our Hoare-triples we can easily prove the following Hoare-consequence rule
|
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
799 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
800 |
\begin{equation}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
801 |
@{thm[mode=Rule] Hoare_consequence}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
802 |
\end{equation}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
803 |
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
804 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
805 |
where
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
806 |
@{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
807 |
@{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}).
|
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
808 |
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
809 |
Like Asperti and Ricciotti with their notion of realisability, we
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
810 |
have set up our Hoare-rules so that we can deal explicitly
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
811 |
with total correctness and non-terminantion, rather than have
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
812 |
notions for partial correctness and termination. Although the latter
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
813 |
would allow us to reason more uniformly (only using Hoare-triples),
|
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
814 |
we prefer our definitions because we can derive below some simple
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
815 |
Hoare-rules for sequentially composed Turing programs. In this way
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
816 |
we can reason about the correctness of @{term "tcopy_begin"}, for
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
817 |
example, completely separately from @{term "tcopy_loop"} and @{term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
818 |
"tcopy_end"}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
819 |
|
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
820 |
It is realatively straightforward to prove that the Turing program
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
821 |
@{term "dither"} shown in \eqref{dither} is correct. This program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
822 |
should be the ``identity'' when started with a standard tape representing
|
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
823 |
@{text "1"} but loops when started with @{text 0} instead, as pictured
|
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
824 |
below.
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
825 |
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
826 |
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
827 |
\begin{center}
|
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
828 |
\begin{tabular}{l@ {\hspace{3mm}}lcl}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
829 |
& \multicolumn{1}{c}{start tape}\\[1mm]
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
830 |
\raisebox{2mm}{halting case:} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
831 |
\begin{tikzpicture}[scale=0.8]
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
832 |
\draw[very thick] (-2,0) -- ( 0.75,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
833 |
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
834 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
835 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
836 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
837 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
838 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
839 |
\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
|
840 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
841 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
842 |
\node [anchor=base] at (-1.7,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
843 |
\end{tikzpicture}
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
844 |
& \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
845 |
\begin{tikzpicture}[scale=0.8]
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
846 |
\draw[very thick] (-2,0) -- ( 0.75,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
847 |
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
848 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
849 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
850 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
851 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
852 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
853 |
\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
|
854 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
855 |
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
856 |
\node [anchor=base] at (-1.7,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
857 |
\end{tikzpicture}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
858 |
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
859 |
\raisebox{2mm}{non-halting case:} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
860 |
\begin{tikzpicture}[scale=0.8]
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
861 |
\draw[very thick] (-2,0) -- ( 0.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
862 |
\draw[very thick] (-2,0.5) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
863 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
864 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
865 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
866 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
867 |
\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
|
868 |
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
869 |
\node [anchor=base] at (-1.7,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
870 |
\end{tikzpicture}
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
871 |
& \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
872 |
\raisebox{2mm}{loops}
|
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
873 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
874 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
875 |
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
876 |
\noindent
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
877 |
We can prove the following Hoare-statements:
|
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
878 |
|
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
879 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
880 |
\begin{tabular}{l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
881 |
@{thm dither_halts}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
882 |
@{thm dither_loops}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
883 |
\end{tabular}
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
884 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
885 |
|
77
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
886 |
\noindent
|
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
887 |
The first is by a simple calculation. The second is by an induction on the
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
888 |
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
|
889 |
|
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
890 |
The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
891 |
its purpose is to produce the standard tape @{term "(Bks, <(n,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
892 |
n::nat)>)"} when started with @{term "(Bks, <(n::nat)>)"}, that is
|
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
893 |
making a copy of a value on the tape. Reasoning about this program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
894 |
is substantially harder than about @{term dither}. To ease the
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
895 |
burden, we derive the following two Hoare-rules for sequentially
|
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
896 |
composed programs.
|
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
897 |
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
898 |
\begin{center}
|
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
899 |
\begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
900 |
$\inferrule*[Right=@{thm (prem 3) HR1}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
901 |
{@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
902 |
{@{thm (concl) HR1}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
903 |
$ &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
904 |
$
|
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
905 |
\inferrule*[Right=@{thm (prem 3) HR2}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
906 |
{@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
907 |
{@{thm (concl) HR2}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
908 |
$
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
909 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
910 |
\end{center}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
911 |
|
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
912 |
\noindent
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
913 |
The first corresponds to the usual Hoare-rule for composition of two
|
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
914 |
terminating programs. The second rule gives the conditions for when
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
915 |
the first program terminates generating a tape for which the second
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
916 |
program loops. The side-conditions about @{thm (prem 3) HR2} are
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
917 |
needed in order to ensure that the redirection of the halting and
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
918 |
initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"}, respectively, match
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
919 |
up correctly. These Hoare-rules allow us to prove the correctness
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
920 |
of @{term tcopy} by considering the correctness of the components
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
921 |
@{term "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
922 |
in isolation. This simplifies the reasoning considerably, for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
923 |
example when designing decreasing measures for proving the termination
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
924 |
of the programs. We will show the details for the program @{term
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
925 |
"tcopy_begin"}. For the two other programs we refer the reader to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
926 |
our formalisation.
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
927 |
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
928 |
Given the invariants @{term "inv_begin0"},\ldots,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
929 |
@{term "inv_begin4"} shown in Figure~\ref{invbegin}, which
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
930 |
correspond to each state of @{term tcopy_begin}, we define the
|
103
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
931 |
following invariant for the whole @{term tcopy_begin} program:
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
932 |
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
933 |
\begin{figure}[t]
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
934 |
\begin{center}
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
935 |
\begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
936 |
\hline
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
937 |
@{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
938 |
@{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
939 |
@{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
|
100
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
940 |
@{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
941 |
@{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
942 |
& & @{thm (rhs) inv_begin02}\smallskip \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
943 |
\hline
|
100
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
944 |
@{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
945 |
& & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
946 |
@{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
947 |
\hline
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
948 |
@{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
949 |
@{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
950 |
\hline
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
951 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
952 |
\end{center}
|
106
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
953 |
\caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
954 |
@{term tcopy_begin}. Below, the invariants only for the starting and halting states of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
955 |
@{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant the parameter
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
956 |
@{term n} stands for the number
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
957 |
of @{term Oc}s with which the Turing machine is started.}\label{invbegin}
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
958 |
\end{figure}
|
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
959 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
960 |
\begin{center}
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
961 |
\begin{tabular}{rcl}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
962 |
@{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
963 |
@{text "if"} @{thm (prem 1) inv_begin_print(1)} @{text then} @{thm (rhs) inv_begin_print(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
964 |
& & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(2)} @{text then} @{thm (rhs) inv_begin_print(2)} \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
965 |
& & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(3)} @{text then} @{thm (rhs) inv_begin_print(3)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
966 |
& & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(4)} @{text then} @{thm (rhs) inv_begin_print(4)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
967 |
& & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(5)} @{text then} @{thm (rhs) inv_begin_print(5)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
968 |
& & @{text else} @{thm (rhs) inv_begin_print(6)}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
969 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
970 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
971 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
972 |
\noindent
|
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
973 |
This invariant depends on @{term n} representing the number of
|
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
974 |
@{term Oc}s (or encoded number) on the tape. It is not hard (26
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
975 |
lines of automated proof script) to show that for @{term "n >
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
976 |
(0::nat)"} this invariant is preserved under the computation rules
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
977 |
@{term step} and @{term steps}. This gives us partial correctness
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
978 |
for @{term "tcopy_begin"}.
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
979 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
980 |
We next need to show that @{term "tcopy_begin"} terminates. For this
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
981 |
we introduce lexicographically ordered pairs @{term "(n, m)"}
|
106
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
982 |
derived from configurations @{text "(s, (l, r))"}: @{text n} is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
983 |
the state @{text s}, but ordered according to how @{term tcopy_begin} executes
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
984 |
them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
985 |
a strictly decreasing meansure, @{term m} takes the data on the tape into
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
986 |
account and is calculated according to the following measure function:
|
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
987 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
988 |
\begin{center}
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
989 |
\begin{tabular}{rcl}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
990 |
@{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
991 |
@{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\
|
106
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
992 |
& & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
993 |
@{text "("}@{thm (rhs) measure_begin_print(2)}@{text ")"} \\
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
994 |
& & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
995 |
& & @{text else} @{thm (rhs) measure_begin_print(4)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
996 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
997 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
998 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
999 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1000 |
With this in place, we can show that for every starting tape of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1001 |
form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1002 |
machine @{term "tcopy_begin"} will eventually halt (the measure
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1003 |
decreases in each step). Taking this and the partial correctness
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1004 |
proof together, we obtain the left-most Hoare-triple for @{term tcopy_begin}:
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1005 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1006 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1007 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1008 |
@{thm (concl) begin_correct}\hspace{6mm}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1009 |
@{thm (concl) loop_correct}\hspace{6mm}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1010 |
@{thm (concl) end_correct}
|
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1011 |
\end{center}
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1012 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1013 |
\noindent
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1014 |
where we assume @{text "0 < n"} (similar resoning is needed for
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1015 |
the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1016 |
the halting state of @{term tcopy_begin} implies the invariant of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1017 |
the starting state of @{term tcopy_loop}, that is @{term "inv_begin0
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1018 |
n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1019 |
n"}, we can derive the following Hoare-triple for the correctness
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1020 |
of @{term tcopy}:
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1021 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1022 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1023 |
@{thm tcopy_correct}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1024 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1025 |
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1026 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1027 |
That means if we start with a tape of the form @{term "([], <n::nat>)"} then
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1028 |
@{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}, as desired.
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1029 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1030 |
Finally, we are in the position to prove the undecidability of the halting problem.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1031 |
A program @{term p} started with a standard tape containing the (encoded) numbers
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1032 |
@{term ns} will \emph{halt} with a standard tape containging a single (encoded)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1033 |
number is defined as
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1034 |
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1035 |
\begin{center}
|
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1036 |
@{thm haltP_def}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1037 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1038 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1039 |
\noindent
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1040 |
This roughly means we considering only Turing machine programs
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1041 |
representing functions that take some numbers as input and produce a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1042 |
single number as output. For undecidability, the property we are
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1043 |
proving is that there is no Turing machine that can decide in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1044 |
general whether a Turing machine program halts (answer either @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1045 |
0} for halting and @{text 1} for looping). Given our correctness
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1046 |
proofs for @{term dither} and @{term tcopy} shown above, this
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1047 |
non-existence is now relatively straightforward to establish. We first
|
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1048 |
assume there is a coding function, written @{term "code M"}, which
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1049 |
represents a Turing machine @{term "M"} as a natural number. No
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1050 |
further assumptions are made about this coding function. Suppose a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1051 |
Turing machine @{term H} exists such that if started with the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1052 |
standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0},
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1053 |
respectively @{text 1}, depending on whether @{text M} halts when
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1054 |
started with the input tape containing @{term "<ns>"}. This
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1055 |
assumption is formalised as follows---for all @{term M} and all lists of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1056 |
natural numbers @{term ns}:
|
106
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1057 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1058 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1059 |
\begin{tabular}{r}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1060 |
@{thm (prem 2) uncomputable.h_case} implies
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1061 |
@{thm (concl) uncomputable.h_case}\\
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1062 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1063 |
@{thm (prem 2) uncomputable.nh_case} implies
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1064 |
@{thm (concl) uncomputable.nh_case}
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1065 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1066 |
\end{center}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1067 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1068 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1069 |
The contradiction can be derived using the following Turing machine
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1070 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1071 |
\begin{center}
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1072 |
@{thm tcontra_def}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1073 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1074 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1075 |
\noindent
|
116
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1076 |
Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants on the
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1077 |
left, we can derive the following Hoare-pair for @{term tcontra} on the right.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1078 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1079 |
\begin{center}\small
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1080 |
\begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1081 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1082 |
@{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1083 |
@{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1084 |
@{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1085 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1086 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1087 |
\begin{tabular}[b]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1088 |
\raisebox{-20mm}{$\inferrule*{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1089 |
\inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1090 |
{@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1091 |
\\ @{term "{P\<^isub>3} dither \<up>"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1092 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1093 |
{@{term "{P\<^isub>1} tcontra \<up>"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1094 |
$}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1095 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1096 |
\end{tabular}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1097 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1098 |
|
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1099 |
\noindent
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1100 |
This Hoare-pair contradicts our assumption that @{term tcontra} started
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1101 |
with @{term "<(code tcontra)>"} halts.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1102 |
|
116
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1103 |
Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again given the invariants on the
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1104 |
left, we can derive the Hoare-triple for @{term tcontra} on the right.
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1105 |
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1106 |
\begin{center}\small
|
116
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1107 |
\begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}}
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1108 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1109 |
@{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1110 |
@{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1111 |
@{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1112 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1113 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1114 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1115 |
\raisebox{-20mm}{$\inferrule*{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1116 |
\inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1117 |
{@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1118 |
\\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1119 |
}
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1120 |
{@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1121 |
$}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1122 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1123 |
\end{tabular}
|
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1124 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1125 |
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1126 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1127 |
This time the Hoare-triple states that @{term tcontra} terminates
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1128 |
with the ``output'' @{term "<(1::nat)>"}. In both case we come
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1129 |
to an contradiction, which means we have to abondon our assumption
|
112
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1130 |
that there exists a Turing machine @{term H} which can in general decide
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1131 |
whether Turing machines terminate.
|
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1132 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1133 |
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1134 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1135 |
section {* Abacus Machines *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1136 |
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1137 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1138 |
\noindent
|
112
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1139 |
Boolos et al \cite{Boolos87} use abacus machines as a stepping stone
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1140 |
for making it less laborious to write Turing machine
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1141 |
programs. Abacus machines operate over a set of registers $R_0$,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1142 |
$R_1$, \ldots{} each being able to hold an arbitrary large natural
|
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1143 |
number. We use natural numbers to refer to registers; we also use a natural number
|
116
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1144 |
to represent a program counter and jumping ``addresses''. An abacus
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1145 |
program is a list of \emph{instructions} defined by the datatype:
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1146 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1147 |
\begin{center}
|
111
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1148 |
\begin{tabular}{rcl@ {\hspace{10mm}}l}
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1149 |
@{text "i"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1150 |
& $\mid$ & @{term "Dec R\<iota> i"} & if content of $R$ is non-zero,\\
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1151 |
& & & then decrement it by one\\
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1152 |
& & & otherwise jump to instruction $i$\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1153 |
& $\mid$ & @{term "Goto i"} & jump to instruction $i$
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1154 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1155 |
\end{center}
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1156 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1157 |
\noindent
|
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1158 |
For example the program clearing the register $R$ (that is setting
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1159 |
it to @{term "(0::nat)"}) can be defined as follows:
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1160 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1161 |
\begin{center}
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1162 |
@{thm clear.simps[where n="R\<iota>" and e="i", THEN eq_reflection]}
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1163 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1164 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1165 |
\noindent
|
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1166 |
Running such a program means we start with the first instruction
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1167 |
then execute one instructions after the other, unless there is a jump. For
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1168 |
example the second instruction the jump @{term "Goto 0"} in @{term clear} means
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1169 |
we jump back to the first instruction closing the loop. Like with our
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1170 |
Turing machines, we fetch instructions from an abacus program such
|
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1171 |
that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1172 |
this way it is easy to define a function @{term steps} that
|
120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1173 |
executes @{term n} instructions of an abacus program. A \emph{configuration}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1174 |
of an abacus machine is the program counter together with a snapshot of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1175 |
all registers.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1176 |
By convention
|
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1177 |
the value calculated by an abacus program is stored in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1178 |
last register (the register with the highest index).
|
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1179 |
|
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1180 |
The main point of abacus programs is to be able to translate them to
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1181 |
Turing machine programs. Registers and their content are represented by
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1182 |
standard tapes.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1183 |
Because of the jumps in abacus programs, it
|
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1184 |
seems difficult to build Turing machine programs using @{text "\<oplus>"}.
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1185 |
To overcome this difficulty, we calculate a \emph{layout} as follows
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1186 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1187 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1188 |
\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1189 |
@{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1190 |
@{thm (lhs) layout(2)} & @{text "\<equiv>"} & @{thm (rhs) layout(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1191 |
@{thm (lhs) layout(3)} & @{text "\<equiv>"} & @{thm (rhs) layout(3)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1192 |
@{thm (lhs) layout(4)} & @{text "\<equiv>"} & @{thm (rhs) layout(4)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1193 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1194 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1195 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1196 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1197 |
This gives us a list of natural numbers specifying how many states
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1198 |
are needed to translate each abacus instruction. The @{text Goto}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1199 |
instruction is easiest to translate requiring only one state in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1200 |
the corresponding Turing machine:
|
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1201 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1202 |
\begin{center}
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1203 |
@{thm (rhs) tgoto.simps[where n="i"]}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1204 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1205 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1206 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1207 |
where @{term "i"} is the corresponding state in the Turing machine program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1208 |
to jump to. For translating the instruction @{term Inc}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1209 |
one has to remember that the content of the registers are encoded
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1210 |
in the Turing machine as standard tape. Therefore the translated Turing machine
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1211 |
needs to first find the number corresponding to the register @{text "R"}. This needs a machine
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1212 |
with @{term "(2::nat) * R\<iota>"} states and can be constructed as follows:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1213 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1214 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1215 |
\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1216 |
@{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1217 |
@{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1218 |
\multicolumn{3}{@ {}l@ {}}{\hspace{8mm}@{thm (rhs) findnth.simps(2)}}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1219 |
\end{tabular}
|
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1220 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1221 |
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1222 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1223 |
Then we need to increase the ``number'' on the tape by one,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1224 |
and adjust the following registers. By adjusting we only need to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1225 |
replace the first @{term Oc} of each number by @{term Bk} and the last
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1226 |
one from @{term Bk} to @{term Oc}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1227 |
Finally we need to transition the head of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1228 |
Turing machine back into the standard position. This requires a Turing machine
|
118
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1229 |
with 9 states (we omit the details). Similarly for the translation of @{term Dec}, where the
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1230 |
translated Turing machine needs to first check whether the content of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1231 |
corresponding register is @{text 0}. For this we have a Turing machine program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1232 |
with @{text 16} states.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1233 |
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1234 |
Finally, having a Turing machine for each abacus instruction we need
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1235 |
to ``stitch'' the Turing machines together into one so that each
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1236 |
Turing machine component transitions to next one, just like in
|
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1237 |
the abacus programs. One last problem to overcome is that an abacus
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1238 |
program is assumed to calculate a value stored in the last
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1239 |
register. That means we have to append a Turing machine that
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1240 |
``mops up'' the tape (cleaning all @{text Oc}s) except for the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1241 |
last number represented on the tape.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1242 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1243 |
While generating the Turing machine program for an abacus
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1244 |
program is not too difficult to formalise, the problem is that it
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1245 |
contains @{text Goto}s all over the place. The unfortunate result is
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1246 |
are needed to translate each abacus instruction that we cannot
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1247 |
use our Hoare-rules for reasoning about sequentially composed
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1248 |
programs. Instead we have to treat the Turing machine as one
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1249 |
are needed to translate each abacus instruction``block''
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1250 |
and show as invariant that it performs the same operations
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1251 |
as the abacus program. For this we have to show that for each
|
120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1252 |
configuration of an abacus machine the @{term step}-function
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1253 |
is simulated by zero or more steps in our constructed Turing
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1254 |
machine. This leads to a rather large ``monolithic'' overall
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1255 |
correctness proof that on the conceptual level is difficult to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1256 |
break down into smaller components.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1257 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1258 |
%We were able to simplify the proof somewhat
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1259 |
*}
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1260 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1261 |
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1262 |
section {* Recursive Functions and a Universal Turing Machine *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1263 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1264 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1265 |
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1266 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1267 |
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1268 |
(*
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1269 |
section {* Wang Tiles\label{Wang} *}
|
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1270 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1271 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1272 |
Used in texture mapings - graphics
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1273 |
*}
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1274 |
*)
|
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1275 |
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1276 |
section {* Conclusion *}
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1277 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1278 |
text {*
|
114
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1279 |
We have formalised the main results from three chapters in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1280 |
textbook by Boolos et al \cite{Boolos87}. Following in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1281 |
footsteps of another paper \cite{Nipkow98} formalising the results
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1282 |
from a textbook, we could have titled our paper ``Boolos et al are
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1283 |
(almost) Right''. We have not attempted to formalise everything
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1284 |
precisely as Boolos et al present it, but find definitions that make
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1285 |
mechanised proofs manageable. We have found a small inconsitency in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1286 |
the usage of definitions of \ldots Our interest in this subject
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1287 |
arose from correctness proofs about algorithms where we were unable
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1288 |
to formalise argumants about decidability.
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1289 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1290 |
|
114
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1291 |
The most closely related work is by Norrish \cite{Norrish11}, and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1292 |
Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish bases his
|
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1293 |
approach on $\lambda$-terms. For this he introduced a clever rewriting
|
114
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1294 |
technology based on combinators and de-Bruijn indices for rewriting
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1295 |
modulo $\beta$-equivalence (to keep it manageable)
|
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1296 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1297 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1298 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1299 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1300 |
Later on we need to consider specific Turing machines that
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1301 |
start with a tape in standard form and halt the computation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1302 |
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
|
1303 |
useful to have an operation %@{ term "tape_of_nat_list DUMMY"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1304 |
that translates lists of natural numbers into tapes.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1305 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1306 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1307 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1308 |
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
|
1309 |
and the head pointing to the first one; the Turing machine
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1310 |
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
|
1311 |
``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
|
1312 |
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
|
1313 |
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
|
1314 |
tape corresponding to a value @{term n} and producing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1315 |
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
|
1316 |
clustered on the output tape).
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1317 |
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1318 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1319 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1320 |
Magnus: invariants -- Section 5.4.5 on page 75.
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1321 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1322 |
|
114
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1323 |
There is a tantalising connection with recent work \cite{Jensen13}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1324 |
about verifying X86 assembly code. They observed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1325 |
It remains to be seen whether their specification logic
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1326 |
for assmebly code can make it easier to reason about our Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1327 |
programs.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1328 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1329 |
*}
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1330 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1331 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1332 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1333 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1334 |
end
|
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1335 |
end
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1336 |
(*>*) |