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