271
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 Slides2
|
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 |
declare [[show_question_marks = false]]
|
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 |
hide_const (open) s
|
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 |
abbreviation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
"update2 p a \<equiv> update a p"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
notation (Rule output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
"==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
syntax (Rule output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
("\<^raw:\mbox{>_\<^raw:}\\>/ _")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
notation (Axiom output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
"Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
notation (IfThen output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
syntax (IfThen output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
33 |
"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
34 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
35 |
notation (IfThenNoBox output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
36 |
"==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
syntax (IfThenNoBox output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
41 |
"_asm" :: "prop \<Rightarrow> asms" ("_")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
context uncomputable
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
begin
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
notation (latex output)
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
Cons ("_::_" [48,47] 68) and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
append ("_@_" [65, 64] 65) and
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
Oc ("1") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
Bk ("0") and
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
exponent ("_\<^bsup>_\<^esup>" [107] 109) and
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
inv_begin0 ("I\<^isub>0") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
inv_begin1 ("I\<^isub>1") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
inv_begin2 ("I\<^isub>2") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
inv_begin3 ("I\<^isub>3") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
inv_begin4 ("I\<^isub>4") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
inv_begin ("I\<^bsub>cbegin\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
inv_loop1 ("J\<^isub>1") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
inv_loop0 ("J\<^isub>0") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
inv_end1 ("K\<^isub>1") and
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
inv_end0 ("K\<^isub>0") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
Pr ("Pr\<^isup>_") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
Cn ("Cn\<^isup>_") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
Mn ("Mn\<^isup>_") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
tcopy ("copy") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
tcontra ("contra") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
tape_of ("\<langle>_\<rangle>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
code_tcontra ("code contra") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
tm_comp ("_ ; _")
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
lemma inv_begin_print:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
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
|
75 |
"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
|
76 |
"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
|
77 |
"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
|
78 |
"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
|
79 |
"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
|
80 |
apply(case_tac [!] tp)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
by (auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
lemma inv1:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
85 |
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
|
86 |
unfolding Turing_Hoare.assert_imp_def
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
87 |
unfolding inv_loop1.simps inv_begin0.simps
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
88 |
apply(auto)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
89 |
apply(rule_tac x="1" in exI)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
90 |
apply(auto simp add: replicate.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
91 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
92 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
93 |
lemma inv2:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
94 |
shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
95 |
apply(rule ext)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
apply(case_tac x)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
97 |
apply(simp add: inv_end1.simps)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
98 |
done
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
99 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
100 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
lemma measure_begin_print:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
102 |
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
|
103 |
"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
|
104 |
"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
|
105 |
"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
|
106 |
by (simp_all)
|
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 |
lemma inv_begin01:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
assumes "n > 1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
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
|
111 |
using assms by auto
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
113 |
lemma inv_begin02:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
114 |
assumes "n = 1"
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
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
|
116 |
using assms by auto
|
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 |
(*>*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
120 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
122 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
\renewcommand{\slidecaption}{ITP, 24 July 2013}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
124 |
\newcommand{\bl}[1]{#1}
|
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 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
127 |
\begin{frame}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
128 |
\frametitle{%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
129 |
\begin{tabular}{@ {}c@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
130 |
\\[-3mm]
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
131 |
{\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
132 |
{\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm]
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
\end{tabular}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
134 |
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
135 |
\bigskip\medskip\medskip
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
136 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
137 |
\begin{center}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
\begin{tabular}{c@ {\hspace{1cm}}c}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
139 |
\includegraphics[scale=0.29]{jian.jpg} &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
140 |
\includegraphics[scale=0.034]{xingyuan.jpg} \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
Jian Xu & Xingyuan Zhang\\[-3mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
142 |
\end{tabular}\\[3mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
143 |
\small PLA University of Science and Technology
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
144 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
146 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
Christian Urban\\[0mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
148 |
\small King's College London
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
149 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
150 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
151 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
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 |
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
154 |
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
155 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
156 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
157 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
158 |
\begin{frame}[c]
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
159 |
\frametitle{Why Turing Machines?}%
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
160 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
161 |
\begin{itemize}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
162 |
\item At the beginning, it was just a student project
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
about computability.\smallskip
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
164 |
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
165 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
166 |
\begin{tabular}{c}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
167 |
\includegraphics[scale=0.3]{boolos.jpg}\\[-2mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
168 |
\footnotesize Computability and Logic (5th.~ed)\\[-2mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
\footnotesize Boolos, Burgess and Jeffrey\\[2mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
170 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
171 |
\end{center}
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
172 |
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
\item found an inconsistency in the definition of halting computations
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
174 |
(Chap.~3 vs Chap.~8)
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
175 |
\end{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
176 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
177 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
178 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
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 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
181 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
182 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
183 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
184 |
\begin{frame}[c]
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
185 |
\frametitle{Some Previous Works}%
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
186 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
187 |
\begin{itemize}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
188 |
\item Norrish formalised computability theory in HOL starting
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
189 |
from the lambda-calculus\smallskip
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
190 |
\begin{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
191 |
\item \textcolor{gray}{for technical reasons we could not follow him}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
192 |
\item \textcolor{gray}{some proofs use TMs (Wang tilings)}
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
193 |
\end{itemize}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
194 |
\bigskip
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
195 |
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
\item Asperti and Ricciotti formalised TMs in Matita\smallskip
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
197 |
\begin{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
198 |
\item \textcolor{gray}{no undecidability $\Rightarrow$ interest in complexity}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
199 |
\item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates.}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
200 |
\begin{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
201 |
\textcolor{gray}{"In particular, the fact that the universal machine operates with a different
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
202 |
alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
203 |
\end{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
204 |
\end{itemize}
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
205 |
\end{itemize}
|
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 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
208 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
209 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
210 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
211 |
text_raw {*
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
212 |
\tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
213 |
\tikzstyle{node1}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
214 |
draw=black!50, top color=white, bottom color=black!20]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
215 |
\tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
216 |
draw=red!70, top color=white, bottom color=red!50!black!20]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
217 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
218 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
219 |
\begin{frame}[c]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
220 |
\frametitle{The Big Picture}%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
221 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
222 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
223 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
224 |
\matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
225 |
{ \node (def1) [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
226 |
\node (proof1) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
227 |
\node (alg1) [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
228 |
};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
229 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
230 |
\draw[->,black!50,line width=2mm] (proof1) -- (def1);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
231 |
\draw[<-,black!50,line width=2mm] (proof1) -- (alg1);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
232 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
233 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
234 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
235 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
236 |
\only<2->{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
237 |
\begin{textblock}{3}(8.3,4.0)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
238 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
239 |
\node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
240 |
\draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
241 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
242 |
\end{textblock}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
243 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
244 |
\begin{textblock}{3}(3.1,4.0)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
245 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
246 |
\node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
247 |
\draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
248 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
249 |
\end{textblock}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
250 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
251 |
\only<3->{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
252 |
\begin{textblock}{4}(10.9,9.4)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
253 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
254 |
\draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
255 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
256 |
\end{textblock}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
257 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
258 |
\begin{textblock}{3}(1,10.0)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
259 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
260 |
\draw (0,0) node {\small\begin{tabular}{l}undecidabilty\\of the halting\\ problem\end{tabular}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
261 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
262 |
\end{textblock}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
263 |
|
274
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
264 |
\only<4->{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
265 |
\begin{textblock}{4}(4.2,12.4)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
266 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
267 |
\draw (0,0) node {\begin{tabular}{l}correct UTM by translation\end{tabular}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
268 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
269 |
\end{textblock}}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
270 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
271 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
272 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
273 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
274 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
275 |
text_raw {*
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
276 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
277 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
278 |
\begin{frame}[c]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
279 |
\frametitle{Turing Machines}%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
280 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
281 |
\begin{itemize}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
282 |
\item tapes are lists and contain @{text 0}s or @{text 1}s only
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
283 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
284 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
285 |
\begin{tikzpicture}[scale=1]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
286 |
\draw[very thick] (-3.0,0) -- ( 3.0,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
287 |
\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
|
288 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
289 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
290 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
291 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
292 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
293 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
294 |
\draw[very thick] (-1.75,0) -- (-1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
295 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
296 |
\draw[very thick] ( 3.0,0) -- ( 3.0,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
297 |
\draw[very thick] (-3.0,0) -- (-3.0,0.5);
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
298 |
\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
|
299 |
\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
|
300 |
\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
|
301 |
\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
|
302 |
\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
|
303 |
\draw (-0.25,0.8) -- (-0.25,-0.8);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
304 |
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
305 |
\node [anchor=base] at (-0.85,-0.5) {\small left list\;\;\;\;\mbox{}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
306 |
\node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
307 |
\node [anchor=base] at (0.1,0.7) {\small \;\;head};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
308 |
\node [anchor=base] at (-2.2,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
309 |
\node [anchor=base] at ( 2.3,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
310 |
\end{tikzpicture}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
311 |
\end{center}\pause
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
312 |
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
313 |
\item @{text steps} function:
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
314 |
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
315 |
\begin{quote}\rm
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
316 |
What does the TM claclulate after it has executed @{text n} steps?
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
317 |
\end{quote}\pause
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
318 |
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
319 |
\item designate the @{text 0}-state as "halting state" and remain there
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
320 |
forever, i.e.~have a @{text Nop}-action
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
321 |
\end{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
322 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
323 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
324 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
325 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
326 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
327 |
text_raw {*
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
328 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
329 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
330 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
331 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
332 |
\begin{frame}[c]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
333 |
\frametitle{Register Machines}%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
334 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
335 |
\begin{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
336 |
\item programs are lists of instructions
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
337 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
338 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
339 |
\begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
340 |
@{text "I"} & $::=$ & @{term "Goto L\<iota>"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
341 |
& \textcolor{black!60}{jump to instruction @{text L}}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
342 |
& $\mid$ & @{term "Inc R\<iota>"} & \textcolor{black!60}{increment register @{text "R"} by one}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
343 |
& $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if content of @{text R} is non-zero,}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
344 |
& & & \textcolor{black!60}{then decrement it by one}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
345 |
& & & \textcolor{black!60}{otherwise jump to instruction @{text L}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
346 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
347 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
348 |
\end{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
350 |
\only<2->{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
351 |
\begin{textblock}{4}(0.3,4.2)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
352 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
353 |
\node[ellipse callout, fill=red] at (0, 0){\textcolor{yellow}{Spaghetti Code!}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
354 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
355 |
\end{textblock}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
356 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
357 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
358 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
359 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
360 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
361 |
text_raw {*
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
362 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
363 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
364 |
\begin{frame}[c]
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
365 |
\frametitle{Recursive Functions}%
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
366 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
367 |
\begin{itemize}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
368 |
\item[]
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
369 |
\begin{center}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
370 |
\begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
371 |
@{text "rec"} & $::=$ & @{term "Z"} & \textcolor{black!60}{zero-function}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
372 |
& $\mid$ & @{term "S"} & \textcolor{black!60}{successor-function}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
373 |
& $\mid$ & @{term "id n m"} & \textcolor{black!60}{projection}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
374 |
& $\mid$ & @{term "Cn n f gs"} & \textcolor{black!60}{composition}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
375 |
& $\mid$ & @{term "Pr n f g"} & \textcolor{black!60}{primitive recursion}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
376 |
& $\mid$ & @{term "Mn n f"} & \textcolor{black!60}{minimisation}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
377 |
\end{tabular}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
378 |
\end{center}\bigskip
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
379 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
380 |
\item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
381 |
can be defined by simple recursion\\ (HOL has @{term "Least"})
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
382 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
383 |
\item \small you define
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
384 |
\begin{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
385 |
\item addition, multiplication, logical operations, quantifiers\ldots
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
386 |
\item coding of numbers (Cantor encoding), UTM
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
387 |
\end{itemize}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
388 |
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
389 |
\end{itemize}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
390 |
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
391 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
392 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
393 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
394 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
395 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
396 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
397 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
398 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
399 |
\begin{frame}[c]
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
400 |
\frametitle{Copy Turing Machine}%
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
401 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
402 |
\begin{itemize}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
403 |
\item TM that copies a number on the input tape\smallskip
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
404 |
|
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}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
407 |
\begin{tikzpicture}[scale=0.7]
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
408 |
\node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
409 |
\node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
410 |
\node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
411 |
\node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
412 |
\node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
413 |
\node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$};
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
414 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
415 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
416 |
\begin{scope}[shift={(0.5,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
417 |
\draw[very thick] (-0.25,0) -- ( 1.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
418 |
\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
|
419 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
420 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
421 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
422 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
423 |
\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
|
424 |
\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
|
425 |
\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
|
426 |
\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
|
427 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
428 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
429 |
\begin{scope}[shift={(2.9,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
430 |
\draw[very thick] (-0.25,0) -- ( 2.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
431 |
\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
|
432 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
433 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
434 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
435 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
436 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
437 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
438 |
\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
|
439 |
\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
|
440 |
\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
|
441 |
\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
|
442 |
\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
|
443 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
444 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
445 |
\begin{scope}[shift={(6.8,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
446 |
\draw[very thick] (-0.75,0) -- ( 3.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
447 |
\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
|
448 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
449 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
450 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
451 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
452 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
453 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
454 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
455 |
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
456 |
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
457 |
\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
|
458 |
\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
|
459 |
\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
|
460 |
\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
|
461 |
\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
|
462 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
463 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
464 |
\begin{scope}[shift={(11.7,0)}]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
465 |
\draw[very thick] (-0.75,0) -- ( 3.25,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
466 |
\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
|
467 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
468 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
469 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
470 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
471 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
472 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
473 |
\draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
474 |
\draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
475 |
\draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
476 |
\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
|
477 |
\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
|
478 |
\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
|
479 |
\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
|
480 |
\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
|
481 |
\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
|
482 |
\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
|
483 |
\end{scope}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
484 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
485 |
\end{center}\bigskip
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
486 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
487 |
\footnotesize
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
488 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
489 |
\begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
490 |
\multicolumn{3}{@ {\hspace{-8mm}}l}{\small@{text "copy \<equiv> cbegin ; cloop ; cend"}}\\[4mm]
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
491 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
492 |
@{text cbegin} @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
493 |
\hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
494 |
\hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
495 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
496 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
497 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
498 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
499 |
@{text cloop} @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
500 |
\hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
501 |
\hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>0\<^esub>, 2), (R, 3), (R, 4),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
502 |
\hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>1\<^esub>, 5), (R, 4), (L, 6),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
503 |
\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
|
504 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
505 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
506 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
507 |
@{text cend} @{text "\<equiv>"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
508 |
\hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>1\<^esub>, 3),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
509 |
\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
|
510 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>0\<^esub>, 4), (R, 0),"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
511 |
\hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
512 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
513 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
514 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
515 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
516 |
\end{itemize}
|
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 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
519 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
520 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
521 |
*}
|
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 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
524 |
\definecolor{mygrey}{rgb}{.80,.80,.80}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
525 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
526 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
527 |
\begin{frame}[c]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
528 |
\frametitle{Hoare Logic for TMs}%
|
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 |
\begin{itemize}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
531 |
\item Hoare-triples\onslide<2>{ and Hoare-pairs:}
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
532 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
533 |
\small
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
534 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
535 |
\begin{tabular}{@ {\hspace{-6mm}}c@ {\hspace{-3mm}}c@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
536 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
537 |
\colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
538 |
\hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
539 |
\hspace{7mm}if @{term "P tp"} holds then\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
540 |
\hspace{7mm}@{text "\<exists>"}@{term n}. such that\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
541 |
\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
|
542 |
\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
|
543 |
\end{tabular} &
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
544 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
545 |
\onslide<2>{
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
546 |
\begin{tabular}[t]{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
547 |
\colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
548 |
\hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
549 |
\hspace{7mm}if @{term "P tp"} holds then\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
550 |
\hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
551 |
\end{tabular}}
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
552 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
553 |
\end{center}
|
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 |
\end{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
556 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
557 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
558 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
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 |
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
561 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
562 |
lemmas HR1 =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
563 |
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>
diff
changeset
|
564 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
565 |
lemmas HR2 =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
566 |
Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
567 |
(*>*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
568 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
569 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
570 |
\definecolor{mygrey}{rgb}{.80,.80,.80}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
571 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
572 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
573 |
\begin{frame}[c]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
574 |
\frametitle{Some Derived Rules}%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
575 |
\large
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
576 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
577 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
578 |
@{thm[mode=Rule] Hoare_consequence}\bigskip\bigskip\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
579 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
580 |
\begin{tabular}{@ {\hspace{-5mm}}c@ {\hspace{4mm}}c@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
581 |
$\inferrule*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
582 |
{@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
583 |
{@{thm (concl) HR1}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
584 |
$ &
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
585 |
$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
586 |
\inferrule*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
587 |
{@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
588 |
{@{thm (concl) HR2}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
589 |
$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
590 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
591 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
592 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
593 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
594 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
595 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
596 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
597 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
598 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
599 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
600 |
\begin{frame}[t]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
601 |
\frametitle{Undecidability}%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
602 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
603 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
604 |
@{thm tcontra_def}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
605 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
606 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
607 |
\only<2>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
608 |
\begin{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
609 |
\item Suppose @{text H} decides @{text contra} called with code
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
610 |
of @{text contra} halts, then\smallskip
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
611 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
612 |
\begin{center}\small
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
613 |
\begin{tabular}{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
614 |
\begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
615 |
@{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
616 |
@{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
617 |
@{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
618 |
\end{tabular}\bigskip\bigskip
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
619 |
\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
620 |
\begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
621 |
$\inferrule*{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
622 |
\inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
623 |
{@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
624 |
\\ @{term "{P\<^isub>3} dither \<up>"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
625 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
626 |
{@{term "{P\<^isub>1} tcontra \<up>"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
627 |
$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
628 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
629 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
630 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
631 |
\end{itemize}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
632 |
\only<3>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
633 |
\begin{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
634 |
\item Suppose @{text H} decides @{text contra} called with code
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
635 |
of @{text contra} does \emph{not} halt, then\smallskip
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
636 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
637 |
\begin{center}\small
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
638 |
\begin{tabular}{@ {}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
639 |
\begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
640 |
@{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
641 |
@{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
642 |
@{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
643 |
\end{tabular}\bigskip\bigskip
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
644 |
\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
645 |
\begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
646 |
$\inferrule*{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
647 |
\inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
648 |
{@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
649 |
\\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
650 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
651 |
{@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
652 |
$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
653 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
654 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
655 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
656 |
\end{itemize}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
657 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
658 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
659 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
660 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
661 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
662 |
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
663 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
664 |
\definecolor{mygrey}{rgb}{.80,.80,.80}
|
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 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
667 |
\begin{frame}[c]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
668 |
\frametitle{Hoare Reasoning}%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
669 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
670 |
\begin{itemize}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
671 |
\item reasoning is still quite demanding;\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
672 |
the invariants of the copy-machine:\\[-5mm]\mbox{}
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
673 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
674 |
\footnotesize
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
675 |
\begin{center}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
676 |
\begin{tabular}{@ {\hspace{-5mm}}c@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
677 |
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {\hspace{-0.9cm}}l@ {}}
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
678 |
\hline
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
679 |
@{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
|
680 |
@{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
|
681 |
@{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
|
682 |
@{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
|
683 |
@{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
|
684 |
& & @{thm (rhs) inv_begin02}\smallskip \\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
685 |
\hline
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
686 |
@{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
|
687 |
& & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
688 |
@{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
|
689 |
\hline
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
690 |
@{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
|
691 |
@{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
|
692 |
\hline
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
693 |
\end{tabular}
|
272
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
694 |
\end{tabular}
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
695 |
\end{center}
|
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 |
\end{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
698 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
699 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
700 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
701 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
702 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
703 |
|
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 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
706 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
707 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
708 |
\begin{frame}[c]
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
709 |
\frametitle{Midway Conclusion}%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
710 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
711 |
\begin{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
712 |
\item feels awfully like reasoning about machine code
|
274
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
713 |
\item compositional constructions / reasoning not frictionless
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
714 |
\item sizes
|
274
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
715 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
716 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
717 |
\begin{tabular}{ll}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
718 |
& sizes:\smallskip\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
719 |
UF & 140843 constructors\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
720 |
Reg.~Mach.~ & @{text 2} Mio instructions\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
721 |
UTM & @{text 38} Mio states\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
722 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
723 |
\end{center}\pause
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
724 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
725 |
\item an observation: our treatment of recursive functions is a mini-version
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
726 |
of the work by\\ Myreen \& Owens about deeply embedding HOL
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
727 |
\end{itemize}
|
274
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
728 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
729 |
\only<1>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
730 |
\begin{textblock}{4}(2,13.9)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
731 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
732 |
\draw (0,0) node {\small\begin{tabular}{l}$^\star$old version:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
733 |
RM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
734 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
735 |
\end{textblock}}
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
736 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
737 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
738 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
739 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
740 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
741 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
742 |
text_raw {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
743 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
744 |
\mode<presentation>{
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
745 |
\begin{frame}[c]
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
746 |
\frametitle{Separation Algebra}%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
747 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
748 |
\begin{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
749 |
\item introduced a separation algebra framework for register machines and TMs
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
750 |
\item we can semi-automate the reasoning for our small TMs
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
751 |
\item we can assemble bigger programs out of smaller components\bigskip
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
752 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
753 |
\item looks awfully like ``real'' assembly code\pause
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
754 |
\item Conclusion: we have a playing ground for reasoning about low-level
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
755 |
code; we work on automation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
756 |
\end{itemize}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
757 |
\end{frame}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
758 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
759 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
760 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
761 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
762 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
763 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
764 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
765 |
end
|
273
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
766 |
end
|
271
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
767 |
(*>*) |