7 hide_const (open) s |
7 hide_const (open) s |
8 |
8 |
9 abbreviation |
9 abbreviation |
10 "update2 p a \<equiv> update a p" |
10 "update2 p a \<equiv> update a p" |
11 |
11 |
|
12 notation (Rule output) |
|
13 "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
14 |
|
15 syntax (Rule output) |
|
16 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
17 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
18 |
|
19 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" |
|
20 ("\<^raw:\mbox{>_\<^raw:}\\>/ _") |
|
21 |
|
22 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
23 |
|
24 notation (Axiom output) |
|
25 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") |
|
26 |
|
27 notation (IfThen output) |
|
28 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
29 syntax (IfThen output) |
|
30 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
31 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
32 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
33 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
34 |
|
35 notation (IfThenNoBox output) |
|
36 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
37 syntax (IfThenNoBox output) |
|
38 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
39 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
40 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
41 "_asm" :: "prop \<Rightarrow> asms" ("_") |
|
42 |
|
43 context uncomputable |
|
44 begin |
12 |
45 |
13 notation (latex output) |
46 notation (latex output) |
14 Cons ("_::_" [48,47] 68) and |
47 Cons ("_::_" [48,47] 68) and |
15 append ("_@_" [65, 64] 65) and |
48 append ("_@_" [65, 64] 65) and |
16 Oc ("1") and |
49 Oc ("1") and |
23 inv_begin4 ("I\<^isub>4") and |
56 inv_begin4 ("I\<^isub>4") and |
24 inv_begin ("I\<^bsub>cbegin\<^esub>") and |
57 inv_begin ("I\<^bsub>cbegin\<^esub>") and |
25 inv_loop1 ("J\<^isub>1") and |
58 inv_loop1 ("J\<^isub>1") and |
26 inv_loop0 ("J\<^isub>0") and |
59 inv_loop0 ("J\<^isub>0") and |
27 inv_end1 ("K\<^isub>1") and |
60 inv_end1 ("K\<^isub>1") and |
28 inv_end0 ("K\<^isub>0") |
61 inv_end0 ("K\<^isub>0") and |
29 |
62 recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and |
|
63 Pr ("Pr\<^isup>_") and |
|
64 Cn ("Cn\<^isup>_") and |
|
65 Mn ("Mn\<^isup>_") and |
|
66 tcopy ("copy") and |
|
67 tcontra ("contra") and |
|
68 tape_of ("\<langle>_\<rangle>") and |
|
69 code_tcontra ("code contra") and |
|
70 tm_comp ("_ ; _") |
30 |
71 |
31 |
72 |
32 lemma inv_begin_print: |
73 lemma inv_begin_print: |
33 shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and |
74 shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and |
34 "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and |
75 "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and |
139 |
180 |
140 text_raw {* |
181 text_raw {* |
141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
182 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
142 \mode<presentation>{ |
183 \mode<presentation>{ |
143 \begin{frame}[c] |
184 \begin{frame}[c] |
144 \frametitle{Some Previous Work}% |
185 \frametitle{Some Previous Works}% |
145 |
186 |
146 \begin{itemize} |
187 \begin{itemize} |
147 \item Norrish formalised computability theory in HOL starting |
188 \item Norrish formalised computability theory in HOL starting |
148 from the lambda-calculus |
189 from the lambda-calculus\smallskip |
149 \begin{itemize} |
190 \begin{itemize} |
150 \item \textcolor{gray}{for technical reasons we could not follow him} |
191 \item \textcolor{gray}{for technical reasons we could not follow him} |
151 \item \textcolor{gray}{some proofs use TMs (Wang tilings)} |
192 \item \textcolor{gray}{some proofs use TMs (Wang tilings)} |
152 \end{itemize} |
193 \end{itemize} |
153 |
|
154 |
|
155 |
|
156 \bigskip |
194 \bigskip |
157 |
195 |
158 \item Asperti and Ricciotti formalised TMs in Matita |
196 \item Asperti and Ricciotti formalised TMs in Matita\smallskip |
159 \end{itemize} |
197 \begin{itemize} |
|
198 \item \textcolor{gray}{no undecidability $\Rightarrow$ interest in complexity} |
|
199 \item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates.} |
|
200 \begin{quote} |
|
201 \textcolor{gray}{"In particular, the fact that the universal machine operates with a different |
|
202 alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]} |
|
203 \end{quote} |
|
204 \end{itemize} |
|
205 \end{itemize} |
|
206 |
|
207 \end{frame}} |
|
208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
209 *} |
|
210 |
|
211 text_raw {* |
|
212 \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex] |
|
213 \tikzstyle{node1}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, |
|
214 draw=black!50, top color=white, bottom color=black!20] |
|
215 \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, |
|
216 draw=red!70, top color=white, bottom color=red!50!black!20] |
|
217 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
218 \mode<presentation>{ |
|
219 \begin{frame}[c] |
|
220 \frametitle{The Big Picture}% |
|
221 |
|
222 \begin{center} |
|
223 \begin{tikzpicture} |
|
224 \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm] |
|
225 { \node (def1) [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \& |
|
226 \node (proof1) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \& |
|
227 \node (alg1) [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\ |
|
228 }; |
|
229 |
|
230 \draw[->,black!50,line width=2mm] (proof1) -- (def1); |
|
231 \draw[<-,black!50,line width=2mm] (proof1) -- (alg1); |
|
232 |
|
233 \end{tikzpicture} |
|
234 \end{center} |
|
235 |
|
236 \only<2->{ |
|
237 \begin{textblock}{3}(8.3,4.0) |
|
238 \begin{tikzpicture} |
|
239 \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{}; |
|
240 \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}}; |
|
241 \end{tikzpicture} |
|
242 \end{textblock} |
|
243 |
|
244 \begin{textblock}{3}(3.1,4.0) |
|
245 \begin{tikzpicture} |
|
246 \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{}; |
|
247 \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}}; |
|
248 \end{tikzpicture} |
|
249 \end{textblock}} |
|
250 |
|
251 \only<3->{ |
|
252 \begin{textblock}{4}(10.9,9.4) |
|
253 \begin{tikzpicture} |
|
254 \draw (0,0) node {\begin{tabular}{l}UF\end{tabular}}; |
|
255 \end{tikzpicture} |
|
256 \end{textblock} |
|
257 |
|
258 \begin{textblock}{3}(1,10.0) |
|
259 \begin{tikzpicture} |
|
260 \draw (0,0) node {\small\begin{tabular}{l}undecidabilty\\of the halting\\ problem\end{tabular}}; |
|
261 \end{tikzpicture} |
|
262 \end{textblock}} |
|
263 |
160 |
264 |
161 \end{frame}} |
265 \end{frame}} |
162 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
266 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
163 *} |
267 *} |
164 |
268 |
181 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
285 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
182 \draw[very thick] (-1.25,0) -- (-1.25,0.5); |
286 \draw[very thick] (-1.25,0) -- (-1.25,0.5); |
183 \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); |
287 \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); |
184 \draw[very thick] (-1.75,0) -- (-1.75,0.5); |
288 \draw[very thick] (-1.75,0) -- (-1.75,0.5); |
185 \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); |
289 \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); |
|
290 \draw[very thick] ( 3.0,0) -- ( 3.0,0.5); |
|
291 \draw[very thick] (-3.0,0) -- (-3.0,0.5); |
186 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
292 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
187 \draw[fill] (1.35,0.1) rectangle (1.65,0.4); |
293 \draw[fill] (1.35,0.1) rectangle (1.65,0.4); |
188 \draw[fill] (0.85,0.1) rectangle (1.15,0.4); |
294 \draw[fill] (0.85,0.1) rectangle (1.15,0.4); |
189 \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); |
295 \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); |
190 \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4); |
296 \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4); |
194 \node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list}; |
300 \node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list}; |
195 \node [anchor=base] at (0.1,0.7) {\small \;\;head}; |
301 \node [anchor=base] at (0.1,0.7) {\small \;\;head}; |
196 \node [anchor=base] at (-2.2,0.2) {\ldots}; |
302 \node [anchor=base] at (-2.2,0.2) {\ldots}; |
197 \node [anchor=base] at ( 2.3,0.2) {\ldots}; |
303 \node [anchor=base] at ( 2.3,0.2) {\ldots}; |
198 \end{tikzpicture} |
304 \end{tikzpicture} |
199 \end{center} |
305 \end{center}\pause |
200 |
306 |
201 \item @{text steps} function: |
307 \item @{text steps} function: |
202 |
308 |
203 \begin{quote}\rm |
309 \begin{quote}\rm |
204 What does the TM claclulate after it has executed @{text n} steps? |
310 What does the TM claclulate after it has executed @{text n} steps? |
205 \end{quote}\pause |
311 \end{quote}\pause |
206 |
312 |
207 \item designate the @{text 0}-state as \"halting state\" and remain there |
313 \item designate the @{text 0}-state as "halting state" and remain there |
208 forever, i.e.~have a @{text Nop}-action |
314 forever, i.e.~have a @{text Nop}-action |
209 \end{itemize} |
315 \end{itemize} |
210 |
316 |
211 \end{frame}} |
317 \end{frame}} |
212 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
318 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
213 *} |
319 *} |
214 |
320 |
215 text_raw {* |
321 text_raw {* |
|
322 |
|
323 |
216 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
324 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
217 \mode<presentation>{ |
325 \mode<presentation>{ |
218 \begin{frame}[c] |
326 \begin{frame}[c] |
219 \frametitle{Register Machines}% |
327 \frametitle{Register Machines}% |
220 |
328 |
221 \begin{itemize} |
329 \begin{itemize} |
222 \item instructions |
330 \item programs are lists of instructions |
223 |
331 |
224 \begin{center} |
332 \begin{center} |
225 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
333 \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l} |
226 @{text "I"} & $::=$ & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\ |
334 @{text "I"} & $::=$ & @{term "Goto L\<iota>"} |
227 & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & if content of @{text R} is non-zero,\\ |
335 & \textcolor{black!60}{jump to instruction @{text L}}\\[1mm] |
228 & & & then decrement it by one\\ |
336 & $\mid$ & @{term "Inc R\<iota>"} & \textcolor{black!60}{increment register @{text "R"} by one}\\[1mm] |
229 & & & otherwise jump to instruction @{text L}\\ |
337 & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if content of @{text R} is non-zero,}\\ |
230 & $\mid$ & @{term "Goto L\<iota>"} & jump to instruction @{text L} |
338 & & & \textcolor{black!60}{then decrement it by one}\\ |
231 \end{tabular} |
339 & & & \textcolor{black!60}{otherwise jump to instruction @{text L}} |
232 \end{center} |
340 \end{tabular} |
233 |
341 \end{center} |
234 \end{itemize} |
342 \end{itemize} |
235 |
343 |
236 \end{frame}} |
344 \only<2->{ |
237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
345 \begin{textblock}{4}(0.3,4.2) |
238 *} |
346 \begin{tikzpicture} |
239 |
347 \node[ellipse callout, fill=red] at (0, 0){\textcolor{yellow}{Spaghetti Code!}}; |
240 text_raw {* |
348 \end{tikzpicture} |
241 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
349 \end{textblock}} |
242 \mode<presentation>{ |
350 |
243 \begin{frame}[c] |
351 \end{frame}} |
244 \frametitle{Copy Turing Machines}% |
352 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
245 |
353 *} |
246 \begin{itemize} |
354 |
247 \item TM that copies a number on the input tape |
355 text_raw {* |
248 |
356 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
249 |
357 \mode<presentation>{ |
250 \begin{center} |
358 \begin{frame}[c] |
251 \begin{tikzpicture}[scale=0.7] |
359 \frametitle{Recursive Functions}% |
|
360 |
|
361 \begin{itemize} |
|
362 \item[] |
|
363 \begin{center} |
|
364 \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l} |
|
365 @{text "rec"} & $::=$ & @{term "Z"} & \textcolor{black!60}{zero-function}\\[1mm] |
|
366 & $\mid$ & @{term "S"} & \textcolor{black!60}{successor-function}\\[1mm] |
|
367 & $\mid$ & @{term "id n m"} & \textcolor{black!60}{projection}\\[1mm] |
|
368 & $\mid$ & @{term "Cn n f gs"} & \textcolor{black!60}{composition}\\[1mm] |
|
369 & $\mid$ & @{term "Pr n f g"} & \textcolor{black!60}{primitive recursion}\\[1mm] |
|
370 & $\mid$ & @{term "Mn n f"} & \textcolor{black!60}{minimisation} |
|
371 \end{tabular} |
|
372 \end{center}\bigskip |
|
373 |
|
374 \item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\ |
|
375 can be defined by simple recursion\\ (HOL has @{term "Least"}) |
|
376 |
|
377 \item \small you define |
|
378 \begin{itemize} |
|
379 \item addition, multiplication, logical operations, quantifiers\ldots |
|
380 \item coding of numbers (Cantor encoding), UTM |
|
381 \end{itemize} |
|
382 |
|
383 \end{itemize} |
|
384 |
|
385 |
|
386 \end{frame}} |
|
387 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
388 *} |
|
389 |
|
390 text_raw {* |
|
391 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
392 \mode<presentation>{ |
|
393 \begin{frame}[c] |
|
394 \frametitle{Copy Turing Machine}% |
|
395 |
|
396 \begin{itemize} |
|
397 \item TM that copies a number on the input tape\smallskip |
|
398 |
|
399 |
|
400 \begin{center} |
|
401 \begin{tikzpicture}[scale=0.7] |
252 \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; |
402 \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; |
253 \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; |
403 \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; |
254 \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; |
404 \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; |
255 \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$}; |
405 \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$}; |
256 \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$}; |
406 \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$}; |
329 \end{center}\bigskip |
479 \end{center}\bigskip |
330 |
480 |
331 \footnotesize |
481 \footnotesize |
332 \begin{center} |
482 \begin{center} |
333 \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c} |
483 \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c} |
|
484 \multicolumn{3}{@ {\hspace{-8mm}}l}{\small@{text "copy \<equiv> cbegin ; cloop ; cend"}}\\[4mm] |
334 \begin{tabular}[t]{@ {}l@ {}} |
485 \begin{tabular}[t]{@ {}l@ {}} |
335 @{text cbegin} @{text "\<equiv>"}\\ |
486 @{text cbegin} @{text "\<equiv>"}\\ |
336 \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\ |
487 \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\ |
337 \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\ |
488 \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\ |
338 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
489 \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} |
382 \hspace{7mm}if @{term "P tp"} holds then\\ |
533 \hspace{7mm}if @{term "P tp"} holds then\\ |
383 \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\ |
534 \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\ |
384 \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
535 \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
385 \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"} |
536 \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"} |
386 \end{tabular} & |
537 \end{tabular} & |
|
538 |
|
539 \onslide<2>{ |
387 \begin{tabular}[t]{@ {}l@ {}} |
540 \begin{tabular}[t]{@ {}l@ {}} |
388 \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm] |
541 \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm] |
389 \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ |
542 \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ |
390 \hspace{7mm}if @{term "P tp"} holds then\\ |
543 \hspace{7mm}if @{term "P tp"} holds then\\ |
391 \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"} |
544 \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"} |
392 \end{tabular} |
545 \end{tabular}} |
393 \end{tabular} |
546 \end{tabular} |
394 \end{center} |
547 \end{center} |
395 |
548 |
396 \end{itemize} |
549 \end{itemize} |
397 |
550 |
398 \end{frame}} |
551 \end{frame}} |
399 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
552 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
400 *} |
553 *} |
|
554 |
|
555 (*<*) |
|
556 lemmas HR1 = |
|
557 Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"] |
|
558 |
|
559 lemmas HR2 = |
|
560 Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"] |
|
561 (*>*) |
|
562 |
|
563 text_raw {* |
|
564 \definecolor{mygrey}{rgb}{.80,.80,.80} |
|
565 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
566 \mode<presentation>{ |
|
567 \begin{frame}[c] |
|
568 \frametitle{Some Derived Rules}% |
|
569 \large |
|
570 |
|
571 \begin{center} |
|
572 @{thm[mode=Rule] Hoare_consequence}\bigskip\bigskip\\ |
|
573 |
|
574 \begin{tabular}{@ {\hspace{-5mm}}c@ {\hspace{4mm}}c@ {}} |
|
575 $\inferrule* |
|
576 {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}} |
|
577 {@{thm (concl) HR1}} |
|
578 $ & |
|
579 $ |
|
580 \inferrule* |
|
581 {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}} |
|
582 {@{thm (concl) HR2}} |
|
583 $ |
|
584 \end{tabular} |
|
585 \end{center} |
|
586 |
|
587 \end{frame}} |
|
588 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
589 *} |
|
590 |
|
591 text_raw {* |
|
592 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
593 \mode<presentation>{ |
|
594 \begin{frame}[t] |
|
595 \frametitle{Undecidability}% |
|
596 |
|
597 \begin{center} |
|
598 @{thm tcontra_def} |
|
599 \end{center} |
|
600 |
|
601 \only<2>{ |
|
602 \begin{itemize} |
|
603 \item Suppose @{text H} decides @{text contra} called with code |
|
604 of @{text contra} halts, then\smallskip |
|
605 |
|
606 \begin{center}\small |
|
607 \begin{tabular}{@ {}l@ {}} |
|
608 \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}} |
|
609 @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
|
610 @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
|
611 @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"} |
|
612 \end{tabular}\bigskip\bigskip |
|
613 \\ |
|
614 \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}} |
|
615 $\inferrule*{ |
|
616 \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}} |
|
617 {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}} |
|
618 \\ @{term "{P\<^isub>3} dither \<up>"} |
|
619 } |
|
620 {@{term "{P\<^isub>1} tcontra \<up>"}} |
|
621 $ |
|
622 \end{tabular} |
|
623 \end{tabular} |
|
624 \end{center} |
|
625 \end{itemize}} |
|
626 \only<3>{ |
|
627 \begin{itemize} |
|
628 \item Suppose @{text H} decides @{text contra} called with code |
|
629 of @{text contra} does \emph{not} halt, then\smallskip |
|
630 |
|
631 \begin{center}\small |
|
632 \begin{tabular}{@ {}l@ {}} |
|
633 \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}} |
|
634 @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
|
635 @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
|
636 @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"} |
|
637 \end{tabular}\bigskip\bigskip |
|
638 \\ |
|
639 \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}} |
|
640 $\inferrule*{ |
|
641 \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}} |
|
642 {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}} |
|
643 \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"} |
|
644 } |
|
645 {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}} |
|
646 $ |
|
647 \end{tabular} |
|
648 \end{tabular} |
|
649 \end{center} |
|
650 \end{itemize}} |
|
651 |
|
652 \end{frame}} |
|
653 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
654 *} |
|
655 |
401 |
656 |
402 text_raw {* |
657 text_raw {* |
403 \definecolor{mygrey}{rgb}{.80,.80,.80} |
658 \definecolor{mygrey}{rgb}{.80,.80,.80} |
404 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
659 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
405 \mode<presentation>{ |
660 \mode<presentation>{ |