--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides3.thy Sat Nov 23 13:23:53 2013 +0000
@@ -0,0 +1,960 @@
+(*<*)
+theory Slides3
+imports "../thys/UTM" "../thys/Abacus_Defs"
+begin
+declare [[show_question_marks = false]]
+
+hide_const (open) s
+
+abbreviation
+ "update2 p a \<equiv> update a p"
+
+notation (Rule output)
+ "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+syntax (Rule output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
+ ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (Axiom output)
+ "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
+notation (IfThen output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (IfThenNoBox output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+context uncomputable
+begin
+
+notation (latex output)
+ Cons ("_::_" [48,47] 68) and
+ append ("_@_" [65, 64] 65) and
+ Oc ("1") and
+ Bk ("0") and
+ exponent ("_\<^bsup>_\<^esup>" [107] 109) and
+ inv_begin0 ("I\<^sub>0") and
+ inv_begin1 ("I\<^sub>1") and
+ inv_begin2 ("I\<^sub>2") and
+ inv_begin3 ("I\<^sub>3") and
+ inv_begin4 ("I\<^sub>4") and
+ inv_begin ("I\<^bsub>cbegin\<^esub>") and
+ inv_loop1 ("J\<^sub>1") and
+ inv_loop0 ("J\<^sub>0") and
+ inv_end1 ("K\<^sub>1") and
+ inv_end0 ("K\<^sub>0") and
+ recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and
+ Pr ("Pr\<^sup>_") and
+ Cn ("Cn\<^sup>_") and
+ Mn ("Mn\<^sup>_") and
+ tcopy ("copy") and
+ tcontra ("contra") and
+ tape_of ("\<langle>_\<rangle>") and
+ code_tcontra ("code contra") and
+ tm_comp ("_ ; _")
+
+
+lemma inv_begin_print:
+ shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
+ "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and
+ "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and
+ "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and
+ "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
+ "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
+apply(case_tac [!] tp)
+by (auto)
+
+
+lemma inv1:
+ shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"
+unfolding Turing_Hoare.assert_imp_def
+unfolding inv_loop1.simps inv_begin0.simps
+apply(auto)
+apply(rule_tac x="1" in exI)
+apply(auto simp add: replicate.simps)
+done
+
+lemma inv2:
+ shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
+apply(rule ext)
+apply(case_tac x)
+apply(simp add: inv_end1.simps)
+done
+
+
+lemma measure_begin_print:
+ shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
+ "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
+ "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and
+ "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
+by (simp_all)
+
+lemma inv_begin01:
+ assumes "n > 1"
+ shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
+using assms by auto
+
+lemma inv_begin02:
+ assumes "n = 1"
+ shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
+using assms by auto
+
+(*>*)
+
+
+
+text_raw {*
+ \renewcommand{\slidecaption}{ITP, 24 July 2013}
+ \newcommand{\bl}[1]{#1}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}
+ \frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\[-3mm]
+ {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm]
+ {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm]
+ \end{tabular}}
+
+ \bigskip\medskip\medskip
+
+ \begin{center}
+ \begin{tabular}{c@ {\hspace{1cm}}c}
+ \includegraphics[scale=0.29]{jian.jpg} &
+ \includegraphics[scale=0.034]{xingyuan.jpg} \\
+ Jian Xu & Xingyuan Zhang\\[-3mm]
+ \end{tabular}\\[3mm]
+ \small PLA University of Science and Technology
+ \end{center}
+
+ \begin{center}
+ Christian Urban\\[0mm]
+ \small King's College London
+ \end{center}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Why Turing Machines?}%
+
+ \begin{itemize}
+ \item At the beginning, it was just a student project
+ about computability.\smallskip
+
+ \begin{center}
+ \begin{tabular}{c}
+ \includegraphics[scale=0.3]{boolos.jpg}\\[-2mm]
+ \footnotesize Computability and Logic (5th.~ed)\\[-2mm]
+ \footnotesize Boolos, Burgess and Jeffrey\\[2mm]
+ \end{tabular}
+ \end{center}
+
+ \item found an inconsistency in the definition of halting computations
+ (Chap.~3 vs Chap.~8)
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Some Previous Works}%
+
+ \begin{itemize}
+ \item Norrish formalised computability theory in HOL starting
+ from the lambda-calculus\smallskip
+ \begin{itemize}
+ \item \textcolor{gray}{for technical reasons we could not follow his work}
+ \item \textcolor{gray}{some proofs use TMs (Wang tilings)}
+ \end{itemize}
+ \bigskip
+
+ \item Asperti and Ricciotti formalised TMs in Matita\smallskip
+ \begin{itemize}
+ \item \textcolor{gray}{no undecidability result $\Rightarrow$ interest in complexity}
+ \item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates}
+ \begin{quote}
+ \textcolor{gray}{"In particular, the fact that the universal machine operates with a different
+ alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]}
+ \end{quote}
+ \end{itemize}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+ \tikzstyle{node1}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
+ draw=black!50, top color=white, bottom color=black!20]
+ \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
+ draw=red!70, top color=white, bottom color=red!50!black!20]
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{The Big Picture}%
+
+ \begin{center}
+ \begin{tikzpicture}
+ \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]
+ { \node (def1) [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&
+ \node (proof1) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&
+ \node (alg1) [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\
+ };
+
+ \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+ \draw[<-,black!50,line width=2mm] (proof1) -- (alg1);
+
+ \end{tikzpicture}
+ \end{center}
+
+ \only<2->{
+ \begin{textblock}{3}(8.3,4.0)
+ \begin{tikzpicture}
+ \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};
+ \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
+ \end{tikzpicture}
+ \end{textblock}
+
+ \begin{textblock}{3}(3.1,4.0)
+ \begin{tikzpicture}
+ \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};
+ \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \only<3->{
+ \begin{textblock}{4}(10.9,9.4)
+ \begin{tikzpicture}
+ \draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};
+ \end{tikzpicture}
+ \end{textblock}
+
+ \begin{textblock}{3}(1,10.0)
+ \begin{tikzpicture}
+ \draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \only<4->{
+ \begin{textblock}{4}(4.2,12.4)
+ \begin{tikzpicture}
+ \draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Turing Machines}%
+
+ \begin{itemize}
+ \item tapes are lists and contain @{text 0}s or @{text 1}s only
+
+ \begin{center}
+\begin{tikzpicture}[scale=1]
+ \draw[very thick] (-3.0,0) -- ( 3.0,0);
+ \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] (-0.75,0) -- (-0.75,0.5);
+ \draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
+ \draw[very thick] (-1.25,0) -- (-1.25,0.5);
+ \draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
+ \draw[very thick] (-1.75,0) -- (-1.75,0.5);
+ \draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
+ \draw[very thick] ( 3.0,0) -- ( 3.0,0.5);
+ \draw[very thick] (-3.0,0) -- (-3.0,0.5);
+ \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+ \draw[fill] (1.35,0.1) rectangle (1.65,0.4);
+ \draw[fill] (0.85,0.1) rectangle (1.15,0.4);
+ \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4);
+ \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4);
+ \draw (-0.25,0.8) -- (-0.25,-0.8);
+ \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
+ \node [anchor=base] at (-0.85,-0.5) {\small left list\;\;\;\;\mbox{}};
+ \node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list};
+ \node [anchor=base] at (0.1,0.7) {\small \;\;head};
+ \node [anchor=base] at (-2.2,0.2) {\ldots};
+ \node [anchor=base] at ( 2.3,0.2) {\ldots};
+ \end{tikzpicture}
+ \end{center}\pause
+
+ \item @{text steps} function:
+
+ \begin{quote}\rm
+ What does the TM calculate after it has executed @{text n} steps?
+ \end{quote}\pause
+
+ \item designate the @{text 0}-state as "halting state" and remain there
+ forever, i.e.~have a @{text Nop}-action
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Register Machines}%
+
+ \begin{itemize}
+ \item programs are lists of instructions
+
+ \begin{center}
+ \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
+ @{text "I"} & $::=$ & @{term "Goto L\<iota>"}
+ & \textcolor{black!60}{jump to instruction @{text L}}\\[1mm]
+ & $\mid$ & @{term "Inc R\<iota>"} & \textcolor{black!60}{increment register @{text "R"} by one}\\[1mm]
+ & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if the content of @{text R} is non-zero,}\\
+ & & & \textcolor{black!60}{then decrement it by one}\\
+ & & & \textcolor{black!60}{otherwise jump to instruction @{text L}}
+ \end{tabular}
+ \end{center}
+ \end{itemize}
+
+ \only<2->{
+ \begin{textblock}{4}(0.3,11.8)
+ \begin{tikzpicture}
+ \node[ellipse callout, fill=red, callout absolute pointer={(-0.2,1)}]
+ at (0, 0){\large\fontspec{Chalkduster}\textcolor{yellow}{Spaghetti Code!}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Recursive Functions}%
+
+ \begin{itemize}
+ \item[]
+ \begin{center}
+ \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
+ @{text "rec"} & $::=$ & @{term "Z"} & \textcolor{black!60}{zero-function}\\[1mm]
+ & $\mid$ & @{term "S"} & \textcolor{black!60}{successor-function}\\[1mm]
+ & $\mid$ & @{term "id n m"} & \textcolor{black!60}{projection}\\[1mm]
+ & $\mid$ & @{term "Cn n f gs"} & \textcolor{black!60}{composition}\\[1mm]
+ & $\mid$ & @{term "Pr n f g"} & \textcolor{black!60}{primitive recursion}\\[1mm]
+ & $\mid$ & @{term "Mn n f"} & \textcolor{black!60}{minimisation}
+ \end{tabular}
+ \end{center}\bigskip
+
+ \item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\
+ can be defined by simple recursion\\ (HOL has @{term "Least"})
+
+ \item \small you define
+ \begin{itemize}
+ \item addition, multiplication, logical operations, quantifiers\ldots
+ \item coding of numbers (Cantor encoding), UF
+ \end{itemize}
+
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Copy Turing Machine}%
+
+ \begin{itemize}
+ \item TM that copies a number on the input tape
+ \begin{center}
+ @{text "copy \<equiv> cbegin ; cloop ; cend"}
+ \end{center}\smallskip
+
+
+ \begin{center}
+ \begin{tikzpicture}[scale=0.7]
+ \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
+ \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
+ \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
+ \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$};
+ \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$};
+ \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$};
+
+
+ \begin{scope}[shift={(0.5,0)}]
+ \draw[very thick] (-0.25,0) -- ( 1.25,0);
+ \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
+ \draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
+ \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+ \draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
+ \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
+ \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
+ \end{scope}
+
+ \begin{scope}[shift={(2.9,0)}]
+ \draw[very thick] (-0.25,0) -- ( 2.25,0);
+ \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
+ \draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
+ \draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
+ \draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
+ \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);
+ \draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
+ \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
+ \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
+ \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
+ \end{scope}
+
+ \begin{scope}[shift={(6.8,0)}]
+ \draw[very thick] (-0.75,0) -- ( 3.25,0);
+ \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
+ \draw[very thick] (-0.75,0) -- (-0.75,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
+ \draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
+ \draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
+ \draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
+ \draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
+ \draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
+ \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+ \draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
+ \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
+ \draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
+ \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
+ \end{scope}
+
+ \begin{scope}[shift={(11.7,0)}]
+ \draw[very thick] (-0.75,0) -- ( 3.25,0);
+ \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
+ \draw[very thick] (-0.75,0) -- (-0.75,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
+ \draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
+ \draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
+ \draw[very thick] ( 2.25,0) -- ( 2.25,0.5);
+ \draw[very thick] ( 2.75,0) -- ( 2.75,0.5);
+ \draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
+ \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+ \draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
+ \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
+ \draw[fill] ( 2.85,0.1) rectangle (3.15,0.4);
+ \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
+ \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
+ \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4);
+ \end{scope}
+ \end{tikzpicture}
+ \end{center}\bigskip
+
+ \footnotesize
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
+ \begin{tabular}[t]{@ {}l@ {}}
+ @{text cbegin} @{text "\<equiv>"}\\
+ \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\
+ \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\
+ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{@ {}l@ {}}
+ @{text cloop} @{text "\<equiv>"}\\
+ \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
+ \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>0\<^esub>, 2), (R, 3), (R, 4),"}\\
+ \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>1\<^esub>, 5), (R, 4), (L, 6),"}\\
+ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{@ {}l@ {}}
+ @{text cend} @{text "\<equiv>"}\\
+ \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>1\<^esub>, 3),"}\\
+ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
+ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>0\<^esub>, 4), (R, 0),"}\\
+ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"}
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ \definecolor{mygrey}{rgb}{.80,.80,.80}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Hoare Logic for TMs}%
+
+ \begin{itemize}
+ \item Hoare-triples\onslide<2>{ and Hoare-pairs:}
+
+ \small
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-6mm}}c@ {\hspace{-3mm}}c@ {}}
+ \begin{tabular}[t]{@ {}l@ {}}
+ \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
+ \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
+ \hspace{7mm}if @{term "P tp"} holds then\\
+ \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\
+ \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\
+ \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}
+ \end{tabular} &
+
+ \onslide<2>{
+ \begin{tabular}[t]{@ {}l@ {}}
+ \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
+ \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
+ \hspace{7mm}if @{term "P tp"} holds then\\
+ \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
+ \end{tabular}}
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+(*<*)
+lemmas HR1 =
+ Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"]
+
+lemmas HR2 =
+ Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]
+(*>*)
+
+text_raw {*
+ \definecolor{mygrey}{rgb}{.80,.80,.80}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Some Derived Rules}%
+ \large
+
+ \begin{center}
+ @{thm[mode=Rule] Hoare_consequence}\bigskip\bigskip\\
+
+ \begin{tabular}{@ {\hspace{-5mm}}c@ {\hspace{4mm}}c@ {}}
+ $\inferrule*
+ {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
+ {@{thm (concl) HR1}}
+ $ &
+ $
+ \inferrule*
+ {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
+ {@{thm (concl) HR2}}
+ $
+ \end{tabular}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[b]
+ \frametitle{Undecidability}%
+
+ \begin{textblock}{7}(4,2.4)
+ @{thm tcontra_def}
+ \end{textblock}
+
+ \only<2>{
+ \begin{itemize}
+ \item Suppose @{text H} decides @{text contra} called with the code
+ of @{text contra} halts, then\smallskip
+
+ \begin{center}\small
+ \begin{tabular}{@ {}l@ {}}
+ \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
+ @{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+ @{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+ @{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
+ \end{tabular}\bigskip\bigskip
+ \\
+ \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
+ $\inferrule*{
+ \inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}}
+ {@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}}
+ \\ @{term "{P\<^sub>3} dither \<up>"}
+ }
+ {@{term "{P\<^sub>1} tcontra \<up>"}}
+ $
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+ \end{itemize}}
+ \only<3>{
+ \begin{itemize}
+ \item Suppose @{text H} decides @{text contra} called with the code
+ of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{}
+
+ \begin{center}\small
+ \begin{tabular}{@ {}l@ {}}
+ \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}}
+ @{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+ @{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+ @{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
+ \end{tabular}\bigskip\bigskip
+ \\
+ \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
+ $\inferrule*{
+ \inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}}
+ {@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}}
+ \\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"}
+ }
+ {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}}
+ $
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+ \end{itemize}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ \definecolor{mygrey}{rgb}{.80,.80,.80}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Hoare Reasoning}%
+
+ \begin{itemize}
+ \item reasoning is quite demanding, e.g.~the invariants
+ of the copy-machine:\\[-5mm]\mbox{}
+
+ \footnotesize
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-5mm}}c@ {}}
+ \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {\hspace{-0.9cm}}l@ {}}
+ \hline
+ @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
+ @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
+ @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
+ @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
+ @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
+ & & @{thm (rhs) inv_begin02}\smallskip \\
+ \hline
+ @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
+ & & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
+ @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
+ \hline
+ @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
+ @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
+ \hline
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Midway Conclusion}%
+
+ \begin{itemize}
+ \item feels awfully like reasoning about machine code
+ \item compositional constructions / reasoning is not at all frictionless
+ \item sizes
+
+ \begin{center}
+ \begin{tabular}{ll}
+ & sizes:\smallskip\\
+ UF & @{text 140843} constructors\\
+ URM & @{text 2} Mio instructions\\
+ UTM & @{text 38} Mio states\\
+ \end{tabular}
+ \end{center}\smallskip\pause
+
+ \item an observation: our treatment of recursive functions is a mini-version
+ of the work by\\ Myreen \& Owens about deeply embedding HOL
+ \end{itemize}
+
+ \only<1>{
+ \begin{textblock}{4}(2,13.9)
+ \begin{tikzpicture}
+ \draw (0,0) node {\small\begin{tabular}{l}$^\star$old version:
+ URM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{\begin{tabular}{@ {}c@ {}}\Large Inspiration from other Works\end{tabular}}%
+
+ \onslide<3->{
+ \begin{itemize}
+ \item Jensen, Benton, Kennedy ({\bf 2013}),
+ {\it High-Level Separation Logic for Low-Level Code}\medskip\\
+
+ \item Myreen ({\bf 2008}), {\it Formal Verification of Machine-Code Programs},
+ PhD thesis\medskip
+
+ \item Klein, Kolanski, Boyton ({\bf 2012}), {\it Mechanised Separation Algebra}
+
+ \end{itemize}}
+
+ \only<2->{
+ \begin{textblock}{4}(1.4,0.9)
+ \begin{tikzpicture}
+ \draw (0,0) node {\fontspec{Chalkduster}\textcolor{red!80}{\LARGE Stealing}};
+ \end{tikzpicture}
+ \end{textblock}}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Better Composability}%
+
+ \begin{itemize}
+ \item an idea from Jensen, Benton \& Kennedy who looked at X86
+ assembly programs and macros\bigskip
+
+ \item assembly for TMs:\medskip
+ \begin{center}
+ \begin{tabular}{l}
+ @{text "move_one_left"} @{text "\<equiv>"}\\
+ \hspace{13mm} @{text "\<Lambda> exit."}\\
+ \hspace{16mm} @{text "Inst (L, exit) (L, exit)"} @{text ";"}\\
+ \hspace{16mm} @{text "Label exit"}\\
+ \end{tabular}
+ \end{center}\bigskip\bigskip
+
+ \begin{tabular}{l}
+ $\Rightarrow$ represent "state" labels as functions\\
+ \phantom{$\Rightarrow$} (with bound variables $\Rightarrow$ locality)
+ \end{tabular}
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Better Composability}%
+
+ \begin{center}
+ \begin{tabular}{@ {\hspace{-10mm}}l}
+ @{text "move_left_until_zero"} @{text "\<equiv>"} \\
+ \hspace{31mm} @{text "\<Lambda> start exit."}\\
+ \hspace{36mm} @{text "Label start"} @{text ";"}\\
+ \hspace{36mm} @{text "if_zero exit"} @{text ";"}\\
+ \hspace{36mm} @{text "move_left"} @{text ";"}\\
+ \hspace{36mm} @{text "jmp start"} @{text ";"}\\
+ \hspace{36mm} @{text "Label exit"}\\
+ \end{tabular}
+ \end{center}
+
+ \small
+ \begin{tabular}{l}
+ @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^sub>0, e), (W\<^sub>1, exit); Label exit"}\\
+ \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^sub>0, e), (W\<^sub>1, e)"}
+ \end{tabular}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{{\large The Trouble With Hoare-Triples}}%
+
+ \begin{itemize}
+ \item Whenever we wanted to prove
+
+ \begin{center}
+ \large @{text "{P} p {Q}"}
+ \end{center}\bigskip\medskip
+
+ \item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}
+
+
+
+ \item[@{text "(2)"}] we had to find a termination order proving that @{text p} terminates
+ \textcolor{gray}{(not easy either)}
+ \end{itemize}\pause
+
+ \begin{center}
+ \alert{very little opportunity for automation}
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Separation Algebra}%
+
+ \begin{itemize}
+ \item use some infrastructure introduced by Klein et al in Isabelle/HOL
+ \item and an idea by Myreen\bigskip\bigskip
+
+ \begin{center}
+ \large @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"}\bigskip\bigskip
+ \end{center}
+
+ \item[] @{text "p, c, q"} will be assertions in a separation logic\pause
+
+ \begin{center}
+ e.g.~~@{text "\<lbrace>st i \<star> hd n \<star> ones u v \<star> zero (v + 1)\<rbrace>"}
+ \end{center}
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Separation Triples}%
+
+ \Large
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{-10mm}}l}
+ @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\
+ & @{text "\<forall> cf r."}\\
+ & \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\
+ & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (steps k cf)"}
+ \end{tabular}
+ \end{center}\bigskip\bigskip
+
+ \normalsize
+ @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Automation}%
+
+ \begin{itemize}
+ \item we introduced some tactics for handling sequential programs\bigskip
+
+ \begin{center}
+ @{text "\<lbrace>p\<rbrace> i:[c\<^sub>1 ; ... ; c\<^sub>n]:j \<lbrace>q\<rbrace>"}
+ \end{center}\bigskip\bigskip
+
+ \item for loops we often only have to do inductions on the length
+ of the input (e.g.~how many @{text "1"}s are on the tape)\pause
+
+ \item these macros allow us to completely get rid of register machines
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Conclusion}%
+
+ \begin{itemize}
+ \item What started out as a student project, turned out to be much more
+ fun than first thought.\bigskip
+
+ \item Where can you claim that you proved the correctness of
+ a @{text "38"} Mio instruction program?
+ (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}})
+ \bigskip
+
+ \item We learned a lot about current verification technology for low-level code
+ (we had no infrastructure: CPU model).\bigskip
+
+ \item The existing literature on TMs \& RMs leave out quite a bit of the story
+ (not to mention contains bugs).
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+(*<*)
+end
+end
+(*>*)
\ No newline at end of file