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
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 3
imports "../thys/UTM"
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
126
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
126
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
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 88
findnth ("find'_nth") and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 89
recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 90
Pr ("Pr\<^isup>_") and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 91
Cn ("Cn\<^isup>_") and
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 92
Mn ("Mn\<^isup>_") and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 93
rec_calc_rel ("eval") and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 94
tm_of_rec ("translate")
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 95
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 97
lemma inv_begin_print:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 98
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
+ − 99
"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
+ − 100
"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
+ − 101
"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
+ − 102
"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
+ − 103
"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
+ − 104
apply(case_tac [!] tp)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 105
by (auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 106
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 107
lemma inv1:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 108
shows "0 < n \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 109
unfolding assert_imp_def
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 110
unfolding inv_loop1.simps inv_begin0.simps
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 111
apply(auto)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 112
apply(rule_tac x="1" in exI)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 113
apply(auto simp add: replicate.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 114
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 116
lemma inv2:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 117
shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 118
apply(rule ext)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 119
apply(case_tac x)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 120
apply(simp add: inv_end1.simps)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 121
done
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 122
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 123
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 124
lemma measure_begin_print:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 125
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
+ − 126
"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
+ − 127
"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
+ − 128
"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
+ − 129
by (simp_all)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 130
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 131
declare [[show_question_marks = false]]
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 132
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 133
lemma nats2tape:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 134
shows "<([]::nat list)> = []"
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 135
and "<[n]> = <n>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 136
and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 137
and "<(n, m)> = <n> @ [Bk] @ <m>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 138
and "<[n, m]> = <(n, m)>"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 139
and "<n> = Oc \<up> (n + 1)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 140
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
+ − 141
apply(case_tac ns)
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 142
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
+ − 143
done
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 144
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 145
lemmas HR1 =
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 146
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
+ − 147
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 148
lemmas HR2 =
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 149
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
+ − 150
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 151
lemma inv_begin01:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 152
assumes "n > 1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 153
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
+ − 154
using assms by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 156
lemma inv_begin02:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 157
assumes "n = 1"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 158
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
+ − 159
using assms by auto
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 160
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 161
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 162
lemma layout:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 163
shows "layout_of [] = []"
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 164
and "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 165
and "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)"
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 166
and "layout_of ((Goto l)#is) = 1#(layout_of is)"
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 167
by(auto simp add: layout_of.simps length_of.simps)
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
(*>*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 171
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 172
section {* Introduction *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 173
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 174
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 175
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 176
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 177
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 178
%\noindent
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 179
%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
+ − 180
%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
+ − 181
%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
+ − 182
%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
+ − 183
%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
+ − 184
%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
+ − 185
%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
+ − 186
%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
+ − 187
%algorithms.
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 188
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 189
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 190
\noindent
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 191
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
+ − 192
P}, say, is decidable or not. Decidability of @{text P} usually
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 193
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
+ − 194
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
+ − 195
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
+ − 196
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
+ − 197
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
+ − 198
this limitation previously when we mechanised the correctness proofs
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 199
of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 200
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
+ − 201
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 202
%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
+ − 203
%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
+ − 204
%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
+ − 205
%represented as inductively defined predicates too.
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 206
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 207
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
+ − 208
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
+ − 209
provided such a formalisation for HOL4. He choose the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 210
$\lambda$-calculus as the starting point for his formalisation because
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 211
of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 212
formalisation is a clever infrastructure for reducing
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 213
$\lambda$-terms. He also established the computational equivalence
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 214
between the $\lambda$-calculus and recursive functions. Nevertheless
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 215
he concluded that it would be appealing to have formalisations for
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 216
more operational models of computations, such as Turing machines or
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 217
register machines. One reason is that many proofs in the literature
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 218
use them. He noted however that \cite[Page 310]{Norrish11}:
8
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
\begin{quote}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 221
\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
+ − 222
general fiddliness,\\ Turing machines are an even more
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 223
daunting prospect.''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 224
\end{quote}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 225
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 226
\noindent
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 227
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
+ − 228
formalisation of Turing machines, as well as abacus machines (a kind
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 229
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
+ − 230
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
+ − 231
programs can be completely \emph{unstructured}, behaving similar to
141
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 232
Basic programs containing the infamous goto \cite{Dijkstra68}. This
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 233
precludes in the general case a compositional Hoare-style reasoning
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 234
about Turing programs. We provide such Hoare-rules for when it
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 235
\emph{is} possible to reason in a compositional manner (which is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 236
fortunately quite often), but also tackle the more complicated case
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 237
when we translate abacus programs into Turing programs. This
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 238
reasoning about concrete Turing machine programs is usually
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 239
left out in the informal literature, e.g.~\cite{Boolos87}.
12
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 240
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 241
%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
+ − 242
%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
+ − 243
%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
+ − 244
%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
+ − 245
%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
+ − 246
%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
+ − 247
%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
+ − 248
%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
+ − 249
%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
+ − 250
%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
+ − 251
%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
+ − 252
%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
+ − 253
%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
+ − 254
%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
+ − 255
%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
+ − 256
%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
+ − 257
%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
+ − 258
%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
+ − 259
%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
+ − 260
%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
+ − 261
%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
+ − 262
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 263
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
+ − 264
the work by Asperti and Ricciotti \cite{AspertiRicciotti12}. They
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 265
describe a complete formalisation of Turing machines in the Matita
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 266
theorem prover, including a universal Turing machine. However, they do
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 267
\emph{not} formalise the undecidability of the halting problem since
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 268
their main focus is complexity, rather than computability theory. They
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 269
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
+ − 270
``sufficiently accurate to be directly usable as a guideline for
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 271
formalization'' \cite[Page 2]{AspertiRicciotti12}. For our
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 272
formalisation we follow mainly the proofs from the textbook by Boolos
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 273
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
+ − 274
detailed. Some details are left out however: for example, constructing
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 275
the \emph{copy Turing machine} is left as an exercise to the
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 276
reader---a corresponding correctness proof is not mentioned at all; also \cite{Boolos87}
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 277
only shows how the universal Turing machine is constructed for Turing
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 278
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
+ − 279
generalise this result to $n$-ary functions. Similarly, when compiling
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 280
recursive functions to abacus machines, the textbook again only shows
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 281
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
+ − 282
formalisation we need arbitrary functions. But the general ideas for
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 283
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
+ − 284
%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
+ − 285
%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
+ − 286
%\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
+ − 287
%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
+ − 288
%which help us with such correctness arguments of Turing machines.
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 289
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 290
The main difference between our formalisation and the one by Asperti
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 291
and Ricciotti is that their universal Turing machine uses a different
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 292
alphabet than the machines it simulates. They write \cite[Page
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 293
23]{AspertiRicciotti12}:
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 294
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 295
\begin{quote}\it
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 296
``In particular, the fact that the universal machine operates with a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 297
different alphabet with respect to the machines it simulates is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 298
annoying.''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 299
\end{quote}
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 300
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 301
\noindent
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 302
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
+ − 303
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
+ − 304
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
+ − 305
Traditionally the content of a cell can be any
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 306
character from a finite alphabet. Although computationally equivalent,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 307
the more restrictive notion of Turing machines in \cite{Boolos87} makes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 308
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
+ − 309
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
+ − 310
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
+ − 311
functions are simpler too. Unfortunately, the restrictiveness also makes
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 312
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
+ − 313
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
+ − 314
\cite{AspertiRicciotti12}, instead follow the proof in
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 315
\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
+ − 316
turn recursive functions to abacus machines. The universal Turing
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 317
machine can then be constructed by translating from a recursive function.
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 318
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 319
\smallskip
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 320
\noindent
141
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 321
{\bf Contributions:} We formalised in Isabelle/HOL Turing machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 322
following the description of Boolos et al \cite{Boolos87} where tapes
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 323
only have blank or occupied cells. We mechanise the undecidability of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 324
the halting problem and prove the correctness of concrete Turing
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 325
machines that are needed in this proof; such correctness proofs are
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 326
left out in the informal literature. For reasoning about Turing
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 327
machine programs we derive Hoare-rules. We also construct the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 328
universal Turing machine from \cite{Boolos87} by translating recursive
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 329
functions to abacus machines and abacus machines to Turing
158
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 330
machines. This works essentially like a small, verified compiler
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 331
from recursive functions to Turing machine programs.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 332
When formalising the universal Turing machine,
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 333
we stumbled in \cite{Boolos87} upon an inconsistent use of the definition of
158
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 334
what partial function a Turing machine calculates.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 335
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 336
%Since we have set up in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 337
%Isabelle/HOL a very general computability model and undecidability
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 338
%result, we are able to formalise other results: we describe a proof of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 339
%the computational equivalence of single-sided Turing machines, which
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 340
%is not given in \cite{Boolos87}, but needed for example for
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 341
%formalising the undecidability proof of Wang's tiling problem
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 342
%\cite{Robinson71}. %We are not aware of any other %formalisation of a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 343
%substantial undecidability problem.
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 344
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 345
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 346
section {* Turing Machines *}
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 347
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 348
text {* \noindent
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 349
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
+ − 350
``gliding'' over a potentially infinite tape. Boolos et
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 351
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
+ − 352
or occupied, which we represent by a datatype having two
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 353
constructors, namely @{text Bk} and @{text Oc}. One way to
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 354
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
+ − 355
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
+ − 356
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
+ − 357
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
+ − 358
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
+ − 359
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
+ − 360
is the cell on which the head of the Turing machine currently
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 361
scans. This can be pictured as follows:
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 362
%
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 363
\begin{center}
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 364
\begin{tikzpicture}[scale=0.9]
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 365
\draw[very thick] (-3.0,0) -- ( 3.0,0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 366
\draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 367
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 368
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 369
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 370
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 371
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 372
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 373
\draw[very thick] (-1.75,0) -- (-1.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 374
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 375
\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
+ − 376
\draw[fill] (1.35,0.1) rectangle (1.65,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 377
\draw[fill] (0.85,0.1) rectangle (1.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 378
\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
+ − 379
\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
+ − 380
\draw (-0.25,0.8) -- (-0.25,-0.8);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 381
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 382
\node [anchor=base] at (-0.85,-0.5) {\small left list};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 383
\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
+ − 384
\node [anchor=base] at (0.1,0.7) {\small head};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 385
\node [anchor=base] at (-2.2,0.2) {\ldots};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 386
\node [anchor=base] at ( 2.3,0.2) {\ldots};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 387
\end{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 388
\end{center}
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 389
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 390
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 391
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
+ − 392
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
+ − 393
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
+ − 394
make this formal we define five possible \emph{actions}
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 395
the Turing machine can perform:
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 396
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 397
\begin{center}
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 398
\begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 399
@{text "a"} & $::=$ & @{term "W0"} & (write blank, @{term Bk})\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 400
& $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 401
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 402
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 403
& $\mid$ & @{term L} & (move left)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 404
& $\mid$ & @{term R} & (move right)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 405
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 406
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 407
& $\mid$ & @{term Nop} & (do-nothing operation)\\
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 408
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 409
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 410
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 411
\noindent
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 412
We slightly deviate
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 413
from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12})
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 414
by using the @{term Nop} operation; however its use
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 415
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
+ − 416
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
+ − 417
following tape updating function:
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 418
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 419
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 420
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 421
@{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
+ − 422
@{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
+ − 423
@{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
+ − 424
@{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
+ − 425
@{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
+ − 426
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 427
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 428
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 429
\noindent
89
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 430
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
+ − 431
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
+ − 432
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
+ − 433
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
+ − 434
such that @{term "tl [] == []"} holds. The third clause
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 435
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
+ − 436
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
+ − 437
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
+ − 438
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
+ − 439
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
+ − 440
leaves the the tape unchanged.
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 441
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 442
%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
+ − 443
%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
+ − 444
%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
+ − 445
%\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
+ − 446
%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
+ − 447
%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
+ − 448
%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
+ − 449
%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
+ − 450
%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
+ − 451
%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
+ − 452
%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
+ − 453
%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
+ − 454
%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
+ − 455
%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
+ − 456
%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
+ − 457
%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
+ − 458
%cover uniformly all cases including corner cases.
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 459
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 460
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
+ − 461
%Given
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 462
%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
+ − 463
%presentations, it might be surprising that in a theorem prover we
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 464
%have to select carefully a representation. If we use the naive
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 465
%representation where a Turing machine consists of a finite set of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 466
%states, then we will have difficulties composing two Turing
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 467
%machines: we would need to combine two finite sets of states,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 468
%possibly renaming states apart whenever both machines share
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 469
%states.\footnote{The usual disjoint union operation in Isabelle/HOL
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 470
%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
+ − 471
%quite cumbersome to reason about.
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 472
We follow the choice made in \cite{AspertiRicciotti12}
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 473
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
+ − 474
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
+ − 475
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
+ − 476
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
+ − 477
segment and adjusting some ``next states'' in the other.
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 478
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 479
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
+ − 480
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
+ − 481
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
+ − 482
program, which consists of four instructions
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 483
%
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 484
\begin{equation}
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 485
\begin{tikzpicture}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 486
\node [anchor=base] at (0,0) {@{thm dither_def}};
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 487
\node [anchor=west] at (-1.5,-0.64)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 488
{$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 489
= starting state\end{tabular}}}$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 490
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 491
\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
+ − 492
\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
+ − 493
\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
+ − 494
\end{tikzpicture}
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 495
\label{dither}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 496
\end{equation}
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 497
%
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 498
\noindent
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 499
the reader can see we have organised our Turing machine programs so
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 500
that segments of two pairs belong to a state. The first component of such a
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 501
segment determines what action should be taken and which next state
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 502
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
+ − 503
similarly the second component determines what should be done in
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 504
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
+ − 505
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
+ − 506
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
+ − 507
``halting state''. There are no instructions for the @{text
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 508
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
+ − 509
remain in the @{text 0}-state. Unlike Asperti and Riccioti
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 510
\cite{AspertiRicciotti12}, we have chosen a very concrete
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 511
representation for Turing machine programs, because when constructing a universal
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 512
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
+ − 513
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
+ − 514
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
+ − 515
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 516
Given a program @{term p}, a state
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 517
and the cell being scanned by the head, we need to fetch
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 518
the corresponding instruction from the program. For this we define
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 519
the function @{term fetch}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 520
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 521
\begin{equation}\label{fetch}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 522
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 523
\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
+ − 524
@{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
+ − 525
\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
+ − 526
@{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
+ − 527
\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
+ − 528
\end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 529
\end{equation}
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 530
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 531
\noindent
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 532
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
+ − 533
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
+ − 534
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
+ − 535
(@{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
+ − 536
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
+ − 537
satisfies the following three properties:
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 538
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 539
\begin{center}
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 540
@{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
+ − 541
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 542
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 543
\noindent
75
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 544
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
+ − 545
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
+ − 546
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
+ − 547
the program or being the @{text 0}-state.
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 548
72
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 549
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
+ − 550
concrete representation, this is relatively straightforward, if
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 551
slightly fiddly. We use the following two auxiliary functions:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 552
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 553
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 554
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 555
@{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 556
@{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 557
\end{tabular}
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
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 561
The first adds @{text n} to all states, except the @{text 0}-state,
72
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 562
thus moving all ``regular'' states to the segment starting at @{text
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 563
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
+ − 564
0}-state, thus redirecting all references to the ``halting state''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 565
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
+ − 566
functions in place, we can define the \emph{sequential composition}
79
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 567
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
+ − 568
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 569
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 570
@{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
+ − 571
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 572
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 573
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 574
%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
+ − 575
%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
+ − 576
%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
+ − 577
%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
+ − 578
%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
+ − 579
%an initial segment of the natural numbers.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 580
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 581
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
+ − 582
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
+ − 583
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
+ − 584
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
+ − 585
"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
+ − 586
calculate what the next configuration is by fetching the appropriate
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 587
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
+ − 588
and tape accordingly. This single step of execution is defined as
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 589
the function @{term step}
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 590
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 591
\begin{center}
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 592
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 593
@{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
+ − 594
& & @{text "in (s', update (l, r) a)"}
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 595
\end{tabular}
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 596
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 597
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 598
\noindent
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 599
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
+ − 600
@{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
+ − 601
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
+ − 602
general evaluation function for Turing machines programs. The reason
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 603
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
+ − 604
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
+ − 605
recursive evaluation function that performs exactly @{text n} steps:
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 606
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 607
\begin{center}
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 608
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 609
@{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
+ − 610
@{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
+ − 611
\end{tabular}
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 612
\end{center}
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 613
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 614
\noindent Recall our definition of @{term fetch} (shown in
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 615
\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
+ − 616
case a Turing program takes according to the usual textbook
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 617
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
+ − 618
halts, then in our setting the @{term steps}-evaluation does not
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 619
actually halt, but rather transitions to the @{text 0}-state (the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 620
final state) and remains there performing @{text Nop}-actions until
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 621
@{text n} is reached.
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 622
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 623
\begin{figure}[t]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 624
\begin{center}
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 625
\begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 626
\begin{tabular}[t]{@ {}l@ {}}
92
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 627
@{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 628
\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
+ − 629
\hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W1, 3), (L, 4),"}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 630
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 631
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 632
&
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 633
\begin{tabular}[t]{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 634
@{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 635
\hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 636
\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
+ − 637
\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
+ − 638
\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
+ − 639
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 640
&
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 641
\begin{tabular}[t]{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 642
@{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 643
\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
+ − 644
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 645
\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
+ − 646
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"}
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 647
\end{tabular}
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 648
\end{tabular}\\[2mm]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 649
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 650
\begin{tikzpicture}[scale=0.7]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 651
\node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 652
\node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 653
\node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
98
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 654
\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
+ − 655
\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
+ − 656
\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
+ − 657
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={(0.5,0)}]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 660
\draw[very thick] (-0.25,0) -- ( 1.25,0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 661
\draw[very thick] (-0.25,0.5) -- ( 1.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[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
+ − 667
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 668
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 669
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 670
\end{scope}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 671
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 672
\begin{scope}[shift={(2.9,0)}]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 673
\draw[very thick] (-0.25,0) -- ( 2.25,0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 674
\draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 675
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 676
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 677
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 678
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 679
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 680
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 681
\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
+ − 682
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 683
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 684
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 685
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 686
\end{scope}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 687
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 688
\begin{scope}[shift={(6.8,0)}]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 689
\draw[very thick] (-0.75,0) -- ( 3.25,0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 690
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 691
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 692
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 693
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 694
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 695
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 696
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 697
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 698
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 699
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 700
\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
+ − 701
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 702
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 703
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 704
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 705
\end{scope}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 706
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 707
\begin{scope}[shift={(11.7,0)}]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 708
\draw[very thick] (-0.75,0) -- ( 3.25,0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 709
\draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 710
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 711
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 712
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 713
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 714
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 715
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 716
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 717
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 718
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 719
\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
+ − 720
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 721
\draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 722
\draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 723
\draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 724
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 725
\draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 726
\end{scope}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 727
\end{tikzpicture}\\[-8mm]\mbox{}
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 728
\end{center}
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 729
\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
+ − 730
(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
+ − 731
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
+ − 732
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
+ − 733
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
+ − 734
\label{copy}
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 735
\end{figure}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 736
87
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 737
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 738
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
+ − 739
the left list of the tape is either empty or only contains @{text "Bk"}s, and
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 740
the right list contains some ``clusters'' of @{text "Oc"}s separated by single
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 741
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
+ − 742
encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 743
%
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 744
\begin{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 745
\mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 746
@{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 747
@{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 748
\end{tabular}\hspace{6mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 749
\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
85
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 750
@{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 751
@{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 752
@{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 753
\end{tabular}}\label{standard}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 754
\end{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 755
%
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 756
\noindent
141
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 757
A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 758
@{text l}
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 759
and @{text "n\<^bsub>1...m\<^esub>"}. 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
+ − 760
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
+ − 761
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
+ − 762
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 763
Before we can prove the undecidability of the halting problem for
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 764
our Turing machines working on standard tapes, we have to analyse
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 765
two concrete Turing machine programs and establish that they are
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 766
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
+ − 767
doing''. Such correctness proofs are usually left out in the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 768
informal literature, for example \cite{Boolos87}. The first program
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 769
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
+ − 770
\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
+ − 771
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 772
\begin{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 773
\mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 774
@{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 775
\end{tabular}}\label{tcopy}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 776
\end{equation}
73
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 777
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 778
\noindent
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 779
whose three components are given in Figure~\ref{copy}. For our
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 780
correctness proofs, we introduce the notion of total correctness
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 781
defined in terms of \emph{Hoare-triples}, written @{term "{P} p
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 782
{Q}"}. They implement the idea that a program @{term
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 783
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
+ − 784
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
+ − 785
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
+ − 786
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
+ − 787
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
+ − 788
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
+ − 789
satisfying @{term P} will loop (never transition into the halting
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 790
state). Both notion are formally defined as
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 791
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 792
\begin{center}
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 793
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 794
\begin{tabular}[t]{@ {}l@ {}}
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 795
\colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 796
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 797
\hspace{7mm}if @{term "P (l, r)"} holds then\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 798
\hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 799
\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
+ − 800
\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
+ − 801
\end{tabular} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 802
\begin{tabular}[t]{@ {}l@ {}}
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 803
\colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 804
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 805
\hspace{7mm}if @{term "P (l, r)"} holds then\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 806
\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
+ − 807
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 808
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 809
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 810
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 811
\noindent
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 812
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
+ − 813
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 814
\begin{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 815
@{thm[mode=Rule] Hoare_consequence}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 816
\end{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 817
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 818
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 819
where
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 820
@{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
+ − 821
@{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
+ − 822
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 823
Like Asperti and Ricciotti with their notion of realisability, we
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 824
have set up our Hoare-rules so that we can deal explicitly
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 825
with total correctness and non-termination, rather than have
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 826
notions for partial correctness and termination. Although the latter
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 827
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
+ − 828
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
+ − 829
Hoare-rules for sequentially composed Turing programs. In this way
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 830
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
+ − 831
example, completely separately from @{term "tcopy_loop"} and @{term
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 832
"tcopy_end"}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 833
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 834
It is relatively straightforward to prove that the Turing program
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 835
@{term "dither"} shown in \eqref{dither} is correct. This program
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 836
should be the ``identity'' when started with a standard tape representing
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 837
@{text "1"} but loops when started with the @{text 0}-representation instead, as pictured
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 838
below.
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 839
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 840
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 841
\begin{center}
81
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 842
\begin{tabular}{l@ {\hspace{3mm}}lcl}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 843
& \multicolumn{1}{c}{start tape}\\[1mm]
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 844
\raisebox{2mm}{halting case:} &
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}
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 858
& \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 859
\begin{tikzpicture}[scale=0.8]
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 860
\draw[very thick] (-2,0) -- ( 0.75,0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 861
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 862
\draw[very thick] (-0.25,0) -- (-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.75,0) -- (-0.75,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
\draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 870
\node [anchor=base] at (-1.7,0.2) {\ldots};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 871
\end{tikzpicture}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 872
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 873
\raisebox{2mm}{non-halting case:} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 874
\begin{tikzpicture}[scale=0.8]
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 875
\draw[very thick] (-2,0) -- ( 0.25,0);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 876
\draw[very thick] (-2,0.5) -- ( 0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 877
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 878
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 879
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 880
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 881
\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
+ − 882
\draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 883
\node [anchor=base] at (-1.7,0.2) {\ldots};
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 884
\end{tikzpicture}
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 885
& \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 886
\raisebox{2mm}{loops}
80
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 887
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 888
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 889
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 890
\noindent
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 891
We can prove the following Hoare-statements:
90
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 892
76
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 893
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 894
\begin{tabular}{l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 895
@{thm dither_halts}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 896
@{thm dither_loops}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 897
\end{tabular}
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 898
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 899
77
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 900
\noindent
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 901
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
+ − 902
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
+ − 903
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 904
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
+ − 905
its purpose is to produce the standard tape @{term "(Bks, <(n,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 906
n::nat)>)"} when started with @{term "(Bks, <(n::nat)>)"}, that is
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 907
making a copy of a value @{term n} on the tape. Reasoning about this program
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 908
is substantially harder than about @{term dither}. To ease the
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 909
burden, we derive the following two Hoare-rules for sequentially
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 910
composed programs.
75
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
\begin{center}
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 913
\begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 914
$\inferrule*[Right=@{thm (prem 3) HR1}]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 915
{@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 916
{@{thm (concl) HR1}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 917
$ &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 918
$
94
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 919
\inferrule*[Right=@{thm (prem 3) HR2}]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 920
{@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 921
{@{thm (concl) HR2}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 922
$
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 923
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 924
\end{center}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 925
91
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 926
\noindent
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 927
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
+ − 928
terminating programs. The second rule gives the conditions for when
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 929
the first program terminates generating a tape for which the second
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 930
program loops. The side-conditions about @{thm (prem 3) HR2} are
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 931
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
+ − 932
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
+ − 933
up correctly. These Hoare-rules allow us to prove the correctness
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 934
of @{term tcopy} by considering the correctness of the components
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 935
@{term "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 936
in isolation. This simplifies the reasoning considerably, for
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 937
example when designing decreasing measures for proving the termination
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 938
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
+ − 939
"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
+ − 940
our formalisation.
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 941
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 942
Given the invariants @{term "inv_begin0"},\ldots,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 943
@{term "inv_begin4"} shown in Figure~\ref{invbegin}, which
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 944
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
+ − 945
following invariant for the whole @{term tcopy_begin} program:
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 946
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 947
\begin{figure}[t]
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 948
\begin{center}
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 949
\begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}}
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
@{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
+ − 952
@{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
+ − 953
@{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
+ − 954
@{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
+ − 955
@{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
+ − 956
& & @{thm (rhs) inv_begin02}\smallskip \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 957
\hline
100
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 958
@{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
+ − 959
& & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 960
@{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
+ − 961
\hline
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 962
@{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
+ − 963
@{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
+ − 964
\hline
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 965
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 966
\end{center}
106
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 967
\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
+ − 968
@{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
+ − 969
@{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
+ − 970
@{term n} stands for the number
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 971
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
+ − 972
\end{figure}
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 973
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 974
\begin{center}
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 975
\begin{tabular}{rcl}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 976
@{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 977
@{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
+ − 978
& & @{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
+ − 979
& & @{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
+ − 980
& & @{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
+ − 981
& & @{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
+ − 982
& & @{text else} @{thm (rhs) inv_begin_print(6)}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 983
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 984
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 985
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 986
\noindent
102
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 987
This invariant depends on @{term n} representing the number of
141
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 988
@{term Oc}s on the tape. It is not hard (26
104
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 989
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
+ − 990
(0::nat)"} this invariant is preserved under the computation rules
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 991
@{term step} and @{term steps}. This gives us partial correctness
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 992
for @{term "tcopy_begin"}.
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 993
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 994
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
+ − 995
we introduce lexicographically ordered pairs @{term "(n, m)"}
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 996
derived from configurations @{text "(s, (l, r))"} whereby @{text n} is
106
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 997
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
+ − 998
them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 999
a strictly decreasing measure, @{term m} takes the data on the tape into
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1000
account and is calculated according to the following measure function:
97
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1001
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1002
\begin{center}
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1003
\begin{tabular}{rcl}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1004
@{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1005
@{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
+ − 1006
& & @{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
+ − 1007
@{text "("}@{thm (rhs) measure_begin_print(2)}@{text ")"} \\
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1008
& & @{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
+ − 1009
& & @{text else} @{thm (rhs) measure_begin_print(4)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1010
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1011
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1012
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1013
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1014
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
+ − 1015
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
+ − 1016
machine @{term "tcopy_begin"} will eventually halt (the measure
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1017
decreases in each step). Taking this and the partial correctness
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1018
proof together, we obtain the Hoare-triple shown on the left for @{term tcopy_begin}:
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1019
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1020
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1021
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1022
@{thm (concl) begin_correct}\hspace{6mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1023
@{thm (concl) loop_correct}\hspace{6mm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1024
@{thm (concl) end_correct}
96
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1025
\end{center}
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1026
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1027
\noindent
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1028
where we assume @{text "0 < n"} (similar reasoning is needed for
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1029
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
+ − 1030
the halting state of @{term tcopy_begin} implies the invariant of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1031
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
+ − 1032
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
+ − 1033
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
+ − 1034
of @{term tcopy}:
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1035
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1036
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1037
@{thm tcopy_correct}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1038
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1039
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1040
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1041
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
+ − 1042
@{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
+ − 1043
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1044
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
+ − 1045
A program @{term p} started with a standard tape containing the (encoded) numbers
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1046
@{term ns} will \emph{halt} with a standard tape containing a single (encoded)
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1047
number is defined as
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1048
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1049
\begin{center}
99
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1050
@{thm haltP_def}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1051
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1052
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1053
\noindent
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1054
This roughly means we considering only Turing machine programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1055
representing functions that take some numbers as input and produce a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1056
single number as output. For undecidability, the property we are
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1057
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
+ − 1058
general whether a Turing machine program halts (answer either @{text
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1059
0} for halting or @{text 1} for looping). Given our correctness
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1060
proofs for @{term dither} and @{term tcopy} shown above, this
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1061
non-existence is now relatively straightforward to establish. We first
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1062
assume there is a coding function, written @{term "code M"}, which
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1063
represents a Turing machine @{term "M"} as a natural number. No
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1064
further assumptions are made about this coding function. Suppose a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1065
Turing machine @{term H} exists such that if started with the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1066
standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0},
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1067
respectively @{text 1}, depending on whether @{text M} halts or not when
107
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1068
started with the input tape containing @{term "<ns>"}. This
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1069
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
+ − 1070
natural numbers @{term ns}:
106
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1071
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1072
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1073
\begin{tabular}{r}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1074
@{thm (prem 2) uncomputable.h_case} implies
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1075
@{thm (concl) uncomputable.h_case}\\
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1076
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1077
@{thm (prem 2) uncomputable.nh_case} implies
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1078
@{thm (concl) uncomputable.nh_case}
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1079
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1080
\end{center}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1081
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1082
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1083
The contradiction can be derived using the following Turing machine
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1084
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1085
\begin{center}
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1086
@{thm tcontra_def}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1087
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1088
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1089
\noindent
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1090
Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^isub>1"}\ldots@{text "P\<^isub>3"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1091
shown on the
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1092
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
+ − 1093
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1094
\begin{center}\small
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1095
\begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1096
\begin{tabular}[t]{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1097
@{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
+ − 1098
@{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
+ − 1099
@{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
+ − 1100
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1101
&
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1102
\begin{tabular}[b]{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1103
\raisebox{-20mm}{$\inferrule*{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1104
\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
+ − 1105
{@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1106
\\ @{term "{P\<^isub>3} dither \<up>"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1107
}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1108
{@{term "{P\<^isub>1} tcontra \<up>"}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1109
$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1110
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1111
\end{tabular}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1112
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1113
105
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1114
\noindent
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1115
This Hoare-pair contradicts our assumption that @{term tcontra} started
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1116
with @{term "<(code tcontra)>"} halts.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1117
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1118
Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again, given the invariants
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1119
@{text "Q\<^isub>1"}\ldots@{text "Q\<^isub>3"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1120
shown on the
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1121
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
+ − 1122
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1123
\begin{center}\small
116
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1124
\begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}}
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1125
\begin{tabular}[t]{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1126
@{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
+ − 1127
@{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
+ − 1128
@{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
+ − 1129
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1130
&
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1131
\begin{tabular}[t]{@ {}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1132
\raisebox{-20mm}{$\inferrule*{
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1133
\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
+ − 1134
{@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1135
\\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1136
}
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1137
{@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1138
$}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1139
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1140
\end{tabular}
93
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1141
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1142
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1143
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1144
This time the Hoare-triple states that @{term tcontra} terminates
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1145
with the ``output'' @{term "<(1::nat)>"}. In both case we come
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1146
to a contradiction, which means we have to abandon our assumption
112
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1147
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
+ − 1148
whether Turing machines terminate.
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1149
*}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1150
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1151
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1152
section {* Abacus Machines *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1153
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1154
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1155
\noindent
112
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1156
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
+ − 1157
for making it less laborious to write Turing machine
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1158
programs. Abacus machines operate over a set of registers @{text "R\<^isub>0"},
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1159
@{text "R\<^isub>1"}, \ldots{}, @{text "R\<^isub>n"} each being able to hold an arbitrary large natural
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1160
number. We use natural numbers to refer to registers; we also use a natural number
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1161
to represent a program counter and to represent jumping ``addresses'', for which we
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1162
use the letter @{text l}. An abacus
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1163
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
+ − 1164
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1165
\begin{center}
111
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1166
\begin{tabular}{rcl@ {\hspace{10mm}}l}
142
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1167
@{text "i"} & $::=$ & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1168
& $\mid$ & @{term "Dec R\<iota> l"} & if content of @{text R} is non-zero, then decrement it by one\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1169
& & & otherwise jump to instruction @{text l}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1170
& $\mid$ & @{term "Goto l"} & jump to instruction @{text l}
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1171
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1172
\end{center}
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1173
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1174
\noindent
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1175
For example the program clearing the register @{text R} (that is setting
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1176
it to @{term "(0::nat)"}) can be defined as follows:
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1177
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1178
\begin{center}
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1179
@{thm clear.simps[where n="R\<iota>" and e="l", THEN eq_reflection]}
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1180
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1181
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1182
\noindent
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1183
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
+ − 1184
then execute one instructions after the other, unless there is a jump. For
143
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1185
example the second instruction @{term "Goto 0"} above means
122
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1186
we jump back to the first instruction thereby closing the loop. Like with our
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1187
Turing machines, we fetch instructions from an abacus program such
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1188
that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
122
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1189
this way it is again easy to define a function @{term steps} that
120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1190
executes @{term n} instructions of an abacus program. A \emph{configuration}
122
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1191
of an abacus machine is the current program counter together with a snapshot of
120
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1192
all registers.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1193
By convention
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1194
the value calculated by an abacus program is stored in the
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1195
last register (the one with the highest index in the program).
113
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1196
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1197
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
+ − 1198
Turing machine programs. Registers and their content are represented by
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1199
standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1200
is impossible to build a Turing machine programs out of components
123
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1201
using our @{text "\<oplus>"}-operation shown in the previous section.
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1202
To overcome this difficulty, we calculate a \emph{layout} of an
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1203
abacus program as follows
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1204
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1205
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1206
\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1207
@{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1208
@{thm (lhs) layout(2)} & @{text "\<equiv>"} & @{thm (rhs) layout(2)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1209
@{thm (lhs) layout(3)} & @{text "\<equiv>"} & @{thm (rhs) layout(3)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1210
@{thm (lhs) layout(4)} & @{text "\<equiv>"} & @{thm (rhs) layout(4)}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1211
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1212
\end{center}
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
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1215
This gives us a list of natural numbers specifying how many states
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1216
are needed to translate each abacus instruction. This information
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1217
is needed in order to calculate the state where the Turing program
144
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1218
code of one abacus instruction ends and the next starts.
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1219
The @{text Goto}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1220
instruction is easiest to translate requiring only one state, namely
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1221
the Turing machine program:
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1222
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1223
\begin{center}
144
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1224
@{text "translate_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]}
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1225
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1226
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1227
\noindent
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1228
where @{term "l"} is the state in the Turing machine program
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1229
to jump to. For translating the instruction @{term "Inc R\<iota>"},
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1230
one has to remember that the content of the registers are encoded
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1231
in the Turing machine as a standard tape. Therefore the translated Turing machine
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1232
needs to first find the number corresponding to the content of register
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1233
@{text "R"}. This needs a machine
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1234
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
+ − 1235
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1236
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1237
\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1238
@{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
+ − 1239
@{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1240
\multicolumn{3}{@ {}l@ {}}{\hspace{8mm}@{thm (rhs) findnth.simps(2)}}\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1241
\end{tabular}
115
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1242
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1243
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1244
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1245
Then we need to increase the ``number'' on the tape by one,
144
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1246
and adjust the following ``registers''. For adjusting we only need to
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1247
change the first @{term Oc} of each number to @{term Bk} and the last
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1248
one from @{term Bk} to @{term Oc}.
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1249
Finally, we need to transition the head of the
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1250
Turing machine back into the standard position. This requires a Turing machine
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1251
with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1252
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
+ − 1253
corresponding register is @{text 0}. For this we have a Turing machine program
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1254
with @{text 16} states (again details are omitted).
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1255
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1256
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
+ − 1257
to ``stitch'' the Turing machines together into one so that each
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1258
Turing machine component transitions to next one, just like in
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1259
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
+ − 1260
program is assumed to calculate a value stored in the last
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1261
register (the one with the highest register). That means we have to append a Turing machine that
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1262
``mops up'' the tape (cleaning all @{text Oc}s) except for the
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1263
@{term Oc}s of the last number represented on the tape. This needs
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1264
a Turing machine program with @{text "2 * R + 12"} states, assuming @{text R}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1265
is the number of registers to be ``cleaned''.
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1266
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1267
While generating the Turing machine program for an abacus program is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1268
not too difficult to formalise, the problem is that it contains
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1269
@{text Goto}s all over the place. The unfortunate result is that we
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1270
cannot use our Hoare-rules for reasoning about sequentially composed
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1271
programs (for this each component needs to be completely independent). Instead we
124
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1272
have to treat the translated Turing machine as one ``big block'' and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1273
prove as invariant that it performs
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1274
the same operations as the abacus program. For this we have to show
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1275
that for each configuration of an abacus machine the @{term
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1276
step}-function is simulated by zero or more steps in our translated
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1277
Turing machine. This leads to a rather large ``monolithic''
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1278
correctness proof (4600 loc and 380 sublemmas) that on the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1279
conceptual level is difficult to break down into smaller components.
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1280
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1281
%We were able to simplify the proof somewhat
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1282
*}
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1283
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1284
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1285
section {* Recursive Functions and a Universal Turing Machine *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1286
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1287
text {*
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1288
The main point of recursive functions is that we can relatively
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1289
easily construct a universal Turing machine via a universal
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1290
function. This is different from Norrish \cite{Norrish11} who gives a universal
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1291
function for Church numbers, and also from Asperti and Ricciotti
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1292
\cite{AspertiRicciotti12} who construct a universal Turing machine
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1293
directly, but for simulating Turing machines with a more restricted alphabet.
144
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1294
\emph{Recursive functions} are defined as the datatype
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1295
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1296
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1297
\begin{tabular}{c@ {\hspace{4mm}}c}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1298
\begin{tabular}{rcl@ {\hspace{4mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1299
@{term r} & @{text "::="} & @{term z} & (zero-functions)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1300
& @{text "|"} & @{term s} & (successor-function)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1301
& @{text "|"} & @{term "id n m"} & (projection)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1302
\end{tabular} &
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1303
\begin{tabular}{cl@ {\hspace{4mm}}l}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1304
@{text "|"} & @{term "Cn n r rs"} & (composition)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1305
@{text "|"} & @{term "Pr n r\<^isub>1 r\<^isub>2"} & (primitive recursion)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1306
@{text "|"} & @{term "Mn n r"} & (minimisation)\\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1307
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1308
\end{tabular}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1309
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1310
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1311
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1312
where @{text n} indicates the function expects @{term n} arguments
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1313
(@{text z} and @{term s} expect one argument), and @{text rs} stands
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1314
for a list of recursive functions. Since we know in each case
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1315
the arity, say @{term l}, we can define an inductive evaluation relation that
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1316
relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l},
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1317
to what the result of the recursive function is, say @{text n}. We omit the
133
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1318
definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1319
definition of translating
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1320
recursive functions into abacus programs. We can prove, however, the following
144
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1321
theorem about the translation: If
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1322
@{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
144
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1323
holds for the recursive function @{text r}, then the following Hoare-triple holds
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1324
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1325
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1326
@{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1327
\end{center}
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
\noindent
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1330
for the translated Turing machine @{term "translate r"}. This
144
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1331
means that if the recursive function @{text r} with arguments @{text ns} evaluates
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1332
to @{text n}, then the translated Turing machine if started
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1333
with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
132
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1334
with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1335
153
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1336
Having recursive functions under our belt, we can construct a universal
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1337
function, written @{text UF}. This universal function acts like an interpreter for Turing machines.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1338
It takes two arguments: one is the code of the Turing machine to be interpreted and the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1339
other is the ``packed version'' of the arguments of the Turing machine.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1340
We can then consider how this universal function is translated to a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1341
Turing machine and from this construct the universal Turing machine,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1342
written @{term UTM}. @{text UTM} is defined as
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1343
the composition of the Turing machine that packages the arguments and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1344
the translated recursive
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1345
function @{text UF}:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1346
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1347
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1348
@{text "UTM \<equiv> arg_coding \<oplus> (translate UF)"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1349
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1350
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1351
\noindent
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1352
Suppose
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1353
a Turing program @{term p} is well-formed and when started with the standard
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1354
tape containing the arguments @{term args}, will produce a standard tape
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1355
with ``output'' @{term n}. This assumption can be written as the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1356
Hoare-triple
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1357
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1358
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1359
@{thm (prem 3) UTM_halt_lemma2}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1360
\end{center}
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1361
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1362
\noindent
153
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1363
where we require that the @{term args} stand for a non-empty list. Then the universal Turing
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1364
machine @{term UTM} started with the code of @{term p} and the arguments
153
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1365
@{term args}, calculates the same result, namely
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1366
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1367
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1368
@{thm (concl) UTM_halt_lemma2}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1369
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1370
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1371
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1372
Similarly, if a Turing program @{term p} started with the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1373
standard tape containing @{text args} loops, which is represented
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1374
by the Hoare-pair
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1375
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1376
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1377
@{thm (prem 2) UTM_unhalt_lemma2}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1378
\end{center}
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1379
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1380
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1381
then the universal Turing machine started with the code of @{term p} and the arguments
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1382
@{term args} will also loop
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1383
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1384
\begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1385
@{thm (concl) UTM_unhalt_lemma2}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1386
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1387
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1388
%Analysing the universal Turing machine constructed in \cite{Boolos87} more carefully
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1389
%we can strengthen this result slightly by observing that @{text m} is at most
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1390
%2 in the output tape. This observation allows one to construct a universal Turing machine that works
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1391
%entirely on the left-tape by composing it with a machine that drags the tape
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1392
%two cells to the right. A corollary is that one-sided Turing machines (where the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1393
%tape only extends to the right) are computationally as powerful as our two-sided
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1394
%Turing machines. So our undecidability proof for the halting problem extends
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1395
%also to one-sided Turing machines, which is needed for example in order to
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1396
%formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
149
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1397
154
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1398
While formalising the chapter in \cite{Boolos87} about universal
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1399
Turing machines, an unexpected outcome of our work is that we
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1400
identified an inconsistency in their use of a definition. This is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1401
unexpected since \cite{Boolos87} is a classic textbook which has
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1402
undergone several editions (we used the fifth edition). The central
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1403
idea about Turing machines is that when started with standard tapes
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1404
they compute a partial arithmetic function. The inconsitency arises
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1405
when they define the case when this function should \emph{not} return a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1406
result. They write in Chapter 3, Page 32:
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1407
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1408
\begin{quote}\it
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1409
``If the function that is to be computed assigns no value to the arguments that
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1410
are represented initially on the tape, then the machine either will never halt,
156
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1411
\colorbox{mygrey}{or} will halt in some nonstandard configuration\ldots''
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1412
\end{quote}
126
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1413
146
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1414
\noindent
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1415
Interestingly, they do not implement this definition when constructing
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1416
their universal Turing machine. In Chapter 8, on page 93, a recursive function
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1417
@{term stdh} is defined as:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1418
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1419
\begin{equation}\label{stdh_def}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1420
@{text "stdh(m, x, t) \<equiv> stat(conf(m, x, t)) + nstd(conf(m, x, t))"}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1421
\end{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1422
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1423
\noindent
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1424
where @{text "stat(conf(m, x, t))"} computes the current state of the
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1425
simulated Turing machine, and @{text "nstd(conf(m, x, t))"} returns @{text 1}
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1426
if the tape content is non-standard. If either one evaluates to
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1427
something that is not zero, then @{text "stdh(m, x, t)"} will be not zero, because of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1428
the $+$-operation. One the same page, a function @{text "halt(m, x)"} is defined
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1429
in terms of @{text stdh} for computing the steps the Turing machine needs to
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1430
execute before it halts (in case it halts at all). According to this definition, the simulated
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1431
Turing machine will continue to run after entering the @{text 0}-state
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1432
with a non-standard tape. The consequence of this inconsistency is
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1433
that there exist Turing machines that given some arguments do not compute a value
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1434
according to Chapter 3, but return a proper result according to
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1435
the definition in Chapter 8. One such Turing machine is:
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1436
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1437
%This means that if you encode the plus function but only give one argument,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1438
%then the TM will either loop {\bf or} stop with a non-standard tape
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1439
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1440
%But in the definition of the universal function the TMs will never stop
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1441
%with non-standard tapes.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1442
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1443
%SO the following TM calculates something according to def from chap 8,
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1444
%but not with chap 3. For example:
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1445
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1446
\begin{center}
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1447
@{term "counter_example \<equiv> [(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1448
\end{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1449
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1450
\noindent
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1451
If started with standard tape @{term "([], [Oc])"}, it halts with the
152
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1452
non-standard tape @{term "([Oc], [])"} according to the definition in Chapter 3---so no
155
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1453
result is calculated; but with the standard tape @{term "([], [Oc])"} according to the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1454
definition in Chapter 8. We solve this inconsitency in our formalisation by
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1455
setting up our definitions so that the @{text counter_example} Turing machine does not
157
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1456
produce any result by looping forever fetching @{term Nop}s in state @{text 0}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1457
This solution is different from the definition in Chapter 3, but also
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1458
different from the one in Chapter 8, where the instruction from state @{text 1} is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1459
fetched.
140
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1460
*}
134
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1461
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1462
(*
140
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1463
section {* XYZ *}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1464
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1465
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1466
One of the main objectives of the paper is the construction and verification of Universal Turing machine (UTM). A UTM takes the code of any Turing machine $M$ and its arguments $a_1, a_2, \ldots, a_n$ as input and computes to the same effect as $M$ does on $a_1, a_2, \ldots, a_n$. That is to say:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1467
\begin{enumerate}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1468
\item If $M$ terminates and gives a result on $a_1, a_2, \ldots, a_n$, so does $UTM$ on input
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1469
$
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1470
code(M), a_1, a_1, a_2, \ldots, a_n
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1471
$.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1472
\item If $M$ loops forever on $a_1, a_2, \ldots, a_n$, then $UTM$ does the same on $code (M), a_1, a_1, a_2, \ldots, a_n$.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1473
\end{enumerate}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1474
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1475
The existence of UTM is the cornerstone of {\em Turing Thesis}, which says: any effectively computable function can be computed by a Turing Machine. The evaluation of Turing machine is obviously effective computable (otherwise, Turing machine is not an effect computation model). So, if the evaluation function of Turing machine can not be implemented by a Turing machine, the {\em Turing Thesis} would fail. Although people believe that UTM exists, few have gave one in close form and prove its correctness with the only exception of Asperti.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1476
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1477
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1478
The method to obtain Universal Turing machine (UTM), as hinted by Boolos's book, is first constructing a recursive function recF (named Universal Function), which serves as an interpreter for Turing machine program, and then the UTM is obtained by $translate(recF)$. However, since any particular recursive function only takes fixed number of arguments determined by its construction, no matter how recF is constructed, it can only server as interpret for Turing machines which take the fixed number of arguments as input. Our solution is to precede the $translate(recF)$ with a Turing machine which compacts multiple arguments into one argument using Wang's coding. Now, $recF$ is defined as a function taking two arguments, where the first is the code of Turing machine to be interpreted and the second is the packed arguments.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1479
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1480
The construction of recF roughly follows the idea in the book. Since the book gives no correctness proof of the construction (not even an informal one), we have to formulate the correctness statements and as well as their formal proofs explicitly. As an unexpected outcome of this formulation, we identified one inconsistency in Boolos' book. Every Turing machine is supposed to compute an arithmetic function which is possibly partial. When the TM is started with an argument where the function is undefined, the definition on Chapter 3 (page 32) says:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1481
\begin{quote}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1482
(e) If the function that is to be computed assigns no value to the arguments that are
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1483
represented initially on the tape, then the machine either will never halt, or will
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1484
halt in some nonstandard configuration such as $B_n11111$ or $B11_n111$ or $B11111_n$.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1485
\end{quote}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1486
According to this definition, a TM can signify a non-result either by looping forever or get into state 0 with a nonstandard tape. However, when we were trying to formalize the universal function in Chapter 8, we found the definition given there is not in accordance. On page 93, an recursive function $stdh$ is defined as:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1487
\begin{equation}\label{stdh_def}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1488
stdh(m, x, t) = stat(conf(m, x, t)) + nstd(conf(m, x, t))
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1489
\end{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1490
Where $ stat(conf(m, x, t)) $ computes the current state of the simulated Turing machine, and the $nstd(conf(m, x, t))$ returns $1$ if the tape content is nonstandard. If either one evaluates to nonzero, stdh(m, x, t) will be nonzero, because of the $+$ operation. One the same page, a function $halt(m, x)$ is defined to in terms of $stdh$ to computes the steps the Turing machine needs to execute before halt, which stipulates the TM halts when nstd(conf(m, x, t)) returns $0$. According to this definition, the simulated Turing machine will continue to run after getting into state $0$ with a nonstandard tape. The consequence of this inconsistency is that: there exists Turing machines which computes non-value according to Chapter 3, but returns a proper result according to Chapter 8. One such Truing machine is:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1491
\begin{equation}\label{contrived_tm}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1492
[(L, 0), (L, 2), (R, 2), (R, 0)]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1493
\end{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1494
Starting in a standard configuration (1, [], [Oc]), it goes through the following series of configurations leading to state 0:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1495
\[
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1496
(1, [], [Oc]) \rightsquigarrow (L, 2) \rightsquigarrow (2, [], [Bk, Oc]) \rightsquigarrow (R, 2)\rightsquigarrow (2, [Bk], [Oc]) \rightsquigarrow (R, 0)\rightsquigarrow (0, [Bk, Oc], [])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1497
\]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1498
According to Chapter 3, this Turing machine halts and gives a non-result. According to Chapter 8, it will continue to fetch and execute the next instruction. The fetching function $actn$ and $newstat$ in \eqref{fetch-def} (taken from page 92) takes $q$ as current state and $r$ as the currently scanned cell.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1499
\begin{equation}\label{fetch-def}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1500
\begin{aligned}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1501
actn(m, q, r ) &= ent(m, 4(q - 1) + 2 \cdot scan(r )) \\
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1502
newstat(m, q, r ) & = ent(m, (4(q - 1) + 2 \cdot scan(r )) + 1)
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1503
\end{aligned}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1504
\end{equation}
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1505
For our instance, $q=0$ and $r = 1$. Because $q - 1 = 0 - 1 = 1 - 1 = 0$, the instruction fetched by \eqref{fetch-def} at state $0$ will be the same as if the machine is at state $0$. So the Turing machine will go through the follow execution and halt with a standard tape:
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1506
\[
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1507
(0, [Bk, Oc], []) \rightsquigarrow (L, 0) \rightsquigarrow (0, [Bk], [Oc])
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1508
\]
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1509
In summary, according to Chapter 3, the Turing machine in \eqref{contrived_tm} computes non-result and according to Chapter 8, it computes an identify function.
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1510
*}
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1511
*)
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1512
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1513
(*
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1514
section {* Wang Tiles\label{Wang} *}
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1515
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1516
text {*
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1517
Used in texture mapings - graphics
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1518
*}
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1519
*)
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1520
121
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1521
section {* Conclusion *}
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1522
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1523
text {*
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1524
In previous works we were unable to formalise results about
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1525
computability because in Isabelle/HOL we cannot represent the
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1526
decidability of a predicate @{text P}, say, as the formula @{term "P
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1527
\<or> \<not>P"}. For reasoning about computability we need to formalise a
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1528
concrete model of computations. We could have followed Norrish
153
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1529
\cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory,
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1530
but then we would have to reimplement his infrastructure for
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1531
reducing $\lambda$-terms on the ML-level. We would still need to
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1532
connect his work to Turing machines for proofs that make essential use of them
153
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1533
(for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1534
158
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1535
We therefore have formalised Turing machines in the first place and the main
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1536
computability results from Chapters 3 to 8 in the textbook by Boolos
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1537
et al \cite{Boolos87}. For this we did not need to implement
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1538
anything on the ML-level of Isabelle/HOL. While formalising the six chapters
158
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1539
\cite{Boolos87} we have found an inconsistency in Boolos et al's
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1540
definitions of what function a Turing machine calculates. In
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1541
Chapter 3 they use a definition that states a function is undefined
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1542
if the Turing machine loops \emph{or} halts with a non-standard
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1543
tape. Whereas in Chapter 8 about the universal Turing machine, the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1544
Turing machines will \emph{not} halt unless the tape is in standard
158
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1545
form. If the title had not already been taken in \cite{Nipkow98}, we could
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1546
have titled our paper ``Boolos et al are (almost)
136
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1547
Right''. We have not attempted to formalise everything precisely as
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1548
Boolos et al present it, but use definitions that make our
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1549
mechanised proofs manageable. For example our definition of the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1550
halting state performing @{term Nop}-operations seems to be
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1551
non-standard, but very much suited to a formalisation in a theorem
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1552
prover where the @{term steps}-function needs to be total.
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1553
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1554
%The most closely related work is by Norrish \cite{Norrish11}, and by
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1555
%Asperti and Ricciotti \cite{AspertiRicciotti12}.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1556
Norrish mentions
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1557
that formalising Turing machines would be a ``\emph{daunting prospect}''
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1558
\cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1559
some slick mechanised proofs, our experience is that Turing machines
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1560
are not too daunting if one is only concerned with formalising the
125
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1561
undecidability of the halting problem for Turing machines. This
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1562
took us around 1500 loc of Isar-proofs, which is just one-and-a-half
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1563
times of a mechanised proof pearl about the Myhill-Nerode
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1564
theorem. So our conclusion is that this part is not as daunting
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1565
as we estimated when reading the paper by Norrish \cite{Norrish11}. The work
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1566
involved with constructing a universal Turing machine via recursive
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1567
functions and abacus machines, we agree, is not a project
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1568
one wants to undertake too many times (our formalisation of abacus
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1569
machines and their correct translation is approximately 4300 loc;
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1570
recursive functions 5000 loc and the universal Turing machine 10000 loc).
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1571
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1572
Our work is also very much inspired by the formalisation of Turing
125
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1573
machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1574
Matita theorem prover. It turns out that their notion of
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1575
realisability and our Hoare-triples are very similar, however we
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1576
differ in some basic definitions for Turing machines. Asperti and
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1577
Ricciotti are interested in providing a mechanised foundation for
130
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1578
complexity theory. They formalised a universal Turing machine
125
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1579
(which differs from ours by using a more general alphabet), but did
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1580
not describe an undecidability proof. Given their definitions and
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1581
infrastructure, we expect however this should not be too difficult
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1582
for them.
125
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1583
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1584
For us the most interesting aspects of our work are the correctness
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1585
proofs for Turing machines. Informal presentations of computability
125
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1586
theory often leave the constructions of particular Turing machines
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1587
as exercise to the reader, for example \cite{Boolos87}, deeming
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1588
it to be just a chore. However, as far as we are aware all informal
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1589
presentations leave out any arguments why these Turing machines
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1590
should be correct. This means the reader is left
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1591
with the task of finding appropriate invariants and measures for
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1592
showing the correctness and termination of these Turing machines.
125
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1593
Whenever we can use Hoare-style reasoning, the invariants are
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1594
relatively straightforward and much smaller than for example the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1595
invariants used by Myreen in a correctness proof of a garbage collector
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1596
written in machine code \cite[Page 76]{Myreen09}. However, the invariant
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1597
needed for the abacus proof, where Hoare-style reasoning does not work, is
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1598
similar in size as the one by Myreen and finding a sufficiently
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1599
strong one took us, like Myreen, something on the magnitude of
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1600
weeks.
71
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1601
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1602
Our reasoning about the invariants is not much supported by the
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1603
automation beyond the standard automation tools available in Isabelle/HOL.
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1604
There is however a tantalising connection
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1605
between our work and very recent work \cite{Jensen13} on verifying
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1606
X86 assembly code that might change that. They observed a similar phenomenon with assembly
159
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1607
programs where Hoare-style reasoning is sometimes possible, but
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1608
sometimes it is not. In order to ease their reasoning, they
125
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1609
introduced a more primitive specification logic, on which
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1610
Hoare-rules can be provided for special cases. It remains to be
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1611
seen whether their specification logic for assembly code can make it
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1612
easier to reason about our Turing programs. That would be an
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1613
attractive result, because Turing machine programs are very much
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1614
like assembly programs and it would connect some very classic work on
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1615
Turing machines to very cutting-edge work on machine code
138
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1616
verification. In order to try out such ideas, our formalisation provides the
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1617
``playground''. The code of our formalisation is available from the
145
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1618
Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}.
114
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1619
*}
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1620
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1621
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1622
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1623
(*<*)
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1624
end
109
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
+ − 1625
end
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
+ − 1626
(*>*)