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