--- a/Slides/Slides3.thy Sat Nov 23 13:23:53 2013 +0000
+++ b/Slides/Slides3.thy Sun Nov 24 14:04:04 2013 +0000
@@ -120,7 +120,7 @@
text_raw {*
- \renewcommand{\slidecaption}{ITP, 24 July 2013}
+ \renewcommand{\slidecaption}{Imperial College, 24 November 2013}
\newcommand{\bl}[1]{#1}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -128,8 +128,9 @@
\frametitle{%
\begin{tabular}{@ {}c@ {}}
\\[-3mm]
- {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm]
- {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm]
+ {\fontsize{30}{30}\selectfont{}Turing Machines and}\\[-1mm]
+ {\fontsize{30}{30}\selectfont{}Separation Logic}\\[0mm]
+ {\fontsize{22}{22}\selectfont{}(Work in Progress)}\\[-3mm]
\end{tabular}}
\bigskip\medskip\medskip
@@ -159,8 +160,8 @@
\frametitle{Why Turing Machines?}%
\begin{itemize}
- \item At the beginning, it was just a student project
- about computability.\smallskip
+ \item we wanted to formalise computability theory
+ \item at the beginning, it was just a student project\smallskip
\begin{center}
\begin{tabular}{c}
@@ -174,6 +175,28 @@
(Chap.~3 vs Chap.~8)
\end{itemize}
+ \only<2->{
+ \begin{textblock}{1}(0.7,4)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\normalsize
+ \begin{minipage}{11cm}
+ \begin{quote}\rm
+ \begin{itemize}
+ \item is a fantastic model of low-level code
+ \item completely unstructured\makebox[0mm][10mm]{\mbox{}}\;\;
+ \only<2>{\textcolor{cream}{\fontspec{Chalkduster}Spaghetti Code}}%
+ \only<3->{\textcolor{red}{\fontspec{Chalkduster}Spaghetti Code}}
+ \bigskip
+ \item good testbed for verification techniques
+ \item Can we verify a program with 38 Mio instructions?
+ \item we can delay implementing a concrete machine model (for OS/low-level code verification)
+ \end{itemize}
+ \end{quote}
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
@@ -182,7 +205,10 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{Some Previous Works}%
+ \frametitle{
+ \begin{tabular}{c}Some Previous Works\\[-5mm]
+ \hspace{3.5cm}\small (but not interested in low-level code)
+ \end{tabular}}%
\begin{itemize}
\item Norrish formalised computability theory in HOL starting
@@ -199,7 +225,7 @@
\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]}
+ alphabet with respect to the machines it simulates is annoying." (Asperti and Ricciotti)}
\end{quote}
\end{itemize}
\end{itemize}
@@ -216,53 +242,66 @@
draw=red!70, top color=white, bottom color=red!50!black!20]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}[c]
+ \begin{frame}[t]
\frametitle{The Big Picture}%
+ \mbox{}\\[19mm]
\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}}; \\
+ { \node (tm) [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&
+ \node (reg) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&
+ \node (rf) [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\
};
- \draw[->,black!50,line width=2mm] (proof1) -- (def1);
- \draw[<-,black!50,line width=2mm] (proof1) -- (alg1);
+ \only<2->{\draw[->,black!50,line width=2mm] (reg) -- (tm);}
+ \only<2->{\draw[<-,black!50,line width=2mm] (reg) -- (rf);}
+
+ \only<4->{
+ \draw [<-, black!50,line width=2mm, rounded corners]
+ % start right of digit.east, that is, at the point that is the
+ % linear combination of digit.east and the vector (2mm,0pt). We
+ % use the ($ ... $) notation for computing linear combinations
+ ($ (rf.south) + (0mm,0) $)
+ % Now go down
+ -- ++(0,-2.5)
+ % And back to the left of digit.west
+ -| ($ (tm.south) - (0mm,0) $);}
\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)
+ \only<1->{
+ \begin{textblock}{3}(1,4.9)
\begin{tikzpicture}
\draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};
\end{tikzpicture}
\end{textblock}}
+ \only<2->{
+ \begin{textblock}{3}(8.3,8.4)
+ \begin{tikzpicture}
+ \node at (0,0) [single arrow, shape border rotate=90, 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,8.4)
+ \begin{tikzpicture}
+ \node at (0,0) [single arrow, shape border rotate=90, 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}(12.5,5.8)
+ \begin{tikzpicture}
+ \draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};
+ \end{tikzpicture}
+ \end{textblock}}
+
\only<4->{
- \begin{textblock}{4}(4.2,12.4)
+ \begin{textblock}{4}(3.3,13.3)
\begin{tikzpicture}
\draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};
\end{tikzpicture}
@@ -379,7 +418,7 @@
\end{center}\bigskip
\item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\
- can be defined by simple recursion\\ (HOL has @{term "Least"})
+ \hspace{3mm}can be defined by recursion (HOL has @{term "Least"})
\item \small you define
\begin{itemize}
@@ -524,6 +563,80 @@
*}
text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Dither Machine}%
+
+ \begin{itemize}
+ \item TM that is the identity with @{text "1"} and loops with @{text "0"}
+ \smallskip
+
+\begin{center}
+ \begin{tabular}{l@ {\hspace{3mm}}lcl}
+ & \multicolumn{1}{c}{start tape}\\[1mm]
+ \raisebox{2mm}{halting case:} &
+ \begin{tikzpicture}[scale=0.8]
+ \draw[very thick] (-2,0) -- ( 0.75,0);
+ \draw[very thick] (-2,0.5) -- ( 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] ( 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);
+ \node [anchor=base] at (-1.7,0.2) {\ldots};
+ \end{tikzpicture}
+ & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
+ \begin{tikzpicture}[scale=0.8]
+ \draw[very thick] (-2,0) -- ( 0.75,0);
+ \draw[very thick] (-2,0.5) -- ( 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] ( 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);
+ \node [anchor=base] at (-1.7,0.2) {\ldots};
+ \end{tikzpicture}\\
+
+ \raisebox{2mm}{non-halting case:} &
+ \begin{tikzpicture}[scale=0.8]
+ \draw[very thick] (-2,0) -- ( 0.25,0);
+ \draw[very thick] (-2,0.5) -- ( 0.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);
+ \node [anchor=base] at (-1.7,0.2) {\ldots};
+ \end{tikzpicture}
+ & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &
+ \raisebox{2mm}{loops}
+ \end{tabular}
+ \end{center}\bigskip
+
+ \small
+ \begin{center}
+ \begin{tabular}[t]{@ {}l@ {}}
+ @{text dither} @{text "\<equiv>"} @{text "["}@{text "(W\<^bsub>0\<^esub>, 1), (R, 2), (L, 1), (L, 0)"}@{text "]"}
+ \end{tabular}
+ \end{center}
+
+
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
\definecolor{mygrey}{rgb}{.80,.80,.80}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -609,7 +722,7 @@
\only<2>{
\begin{itemize}
- \item Suppose @{text H} decides @{text contra} called with the code
+ \item Suppose @{text H} decides whether @{text contra} called with the code
of @{text contra} halts, then\smallskip
\begin{center}\small
@@ -634,8 +747,8 @@
\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{}
+ \item Suppose @{text H} decides wether @{text contra} called with the code
+ of @{text contra} does \alert{not} halt, then\\[-8mm]\mbox{}
\begin{center}\small
\begin{tabular}{@ {}l@ {}}
@@ -723,10 +836,8 @@
URM & @{text 2} Mio instructions\\
UTM & @{text 38} Mio states\\
\end{tabular}
- \end{center}\smallskip\pause
+ \end{center}\smallskip
- \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>{
@@ -745,6 +856,35 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
+ \frametitle{{\fontsize{20}{20}\selectfont{}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{\begin{tabular}{@ {}c@ {}}\Large Inspiration from other Works\end{tabular}}%
\onslide<3->{
@@ -777,9 +917,9 @@
\begin{itemize}
\item an idea from Jensen, Benton \& Kennedy who looked at X86
- assembly programs and macros\bigskip
+ assembler programs and macros\bigskip
- \item assembly for TMs:\medskip
+ \item assembler for TMs:\medskip
\begin{center}
\begin{tabular}{l}
@{text "move_one_left"} @{text "\<equiv>"}\\
@@ -829,26 +969,90 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}[c]
- \frametitle{{\large The Trouble With Hoare-Triples}}%
+ \begin{frame}[t]
+ \frametitle{An RM-API with TMs}%
+
+ \begin{center}
+ \begin{tikzpicture}
+ \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]
+ { \node (tm) [node1, minimum size=44mm] {\mbox{}}; \&
+ \node (rf) [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\
+ };
+
+ \draw[->,black!50,line width=2mm] (rf) -- (tm);
+
+ \node [above, rotate=90] at (tm.east) {\textcolor{gray}{Reg.Mach. API}};
+ \node [below right] at (tm.north west) {\textcolor{gray}{Macros}};
+ \node [node1] at (tm) {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}};
+
+
+ \end{tikzpicture}
+ \end{center}
\begin{itemize}
- \item Whenever we wanted to prove
+ \item Suppose the first four registers of an RM contain 1,2,0 and 3, then the encoding is
\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)}
+ \begin{tikzpicture}[scale=1]
+
+ \draw[very thick] (-0.25,0) -- ( 8.25,0);
+ \draw[very thick] (-0.25,0.5) -- ( 8.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[very thick] ( 2.75,0) -- ( 2.75,0.5);
+ \draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
+ \draw[very thick] ( 3.75,0) -- ( 3.75,0.5);
+ \draw[very thick] ( 4.25,0) -- ( 4.25,0.5);
+ \draw[very thick] ( 4.75,0) -- ( 4.75,0.5);
+ \draw[very thick] ( 5.25,0) -- ( 5.25,0.5);
+ \draw[very thick] ( 5.75,0) -- ( 5.75,0.5);
+ \draw[very thick] ( 6.25,0) -- ( 6.25,0.5);
+ \draw[very thick] ( 6.75,0) -- ( 6.75,0.5);
-
-
- \item[@{text "(2)"}] we had to find a termination order proving that @{text p} terminates
- \textcolor{gray}{(not easy either)}
- \end{itemize}\pause
-
+ \draw[fill] (-0.15,0.1) rectangle (0.15,0.4);
+ \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4);
+ \draw[fill] ( 1.35,0.1) rectangle (1.65,0.4);
+ \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
+ \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
+ \draw[fill] ( 3.35,0.1) rectangle (3.65,0.4);
+ \draw[fill] ( 4.35,0.1) rectangle (4.65,0.4);
+ \draw[fill] ( 4.85,0.1) rectangle (5.15,0.4);
+ \draw[fill] ( 5.35,0.1) rectangle (5.65,0.4);
+ \draw[fill] ( 5.85,0.1) rectangle (6.15,0.4);
+ \end{tikzpicture}
+
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Inc a}%
+
\begin{center}
- \alert{very little opportunity for automation}
+ \begin{tabular}{@ {\hspace{-10mm}}l}
+ @{text "Inc a"} @{text "\<equiv>"} \\
+ \hspace{16mm} @{text "locate a"} @{text ";"}\\
+ \hspace{16mm} @{text "right_until_zero"} @{text ";"}\\
+ \hspace{16mm} @{text "move_right"} @{text ";"}\\
+ \hspace{16mm} @{text "shift_right"} @{text ";"}\\
+ \hspace{16mm} @{text "move_left"} @{text ";"}\\
+ \hspace{16mm} @{text "left_until_double_zero"} @{text ";"}\\
+ \hspace{16mm} @{text "write_one"} @{text ";"}\\
+ \hspace{16mm} @{text "left_until_double_zero"} @{text ";"}\\
+ \hspace{16mm} @{text "move_right"} @{text ";"}\\
+ \hspace{16mm} @{text "move_right"}\\
+ \end{tabular}
\end{center}
\end{frame}}
@@ -896,8 +1100,81 @@
\end{center}\bigskip\bigskip
\normalsize
- @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"}
-
+ \begin{center}
+ @{text "\<lbrace> st i \<star> hd v \<star> zero u \<star> ones (u + 1) v \<rbrace>"}\\
+ @{text "i:[left_until_zero]:j"}\\
+ @{text "\<lbrace> st j \<star> hd u \<star> zero u \<star> ones (u + 1) v \<rbrace>"}\\
+ \end{center}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Inductions over \textit{ones}}%
+
+ \begin{itemize}
+ \item What most simplifies the work is that we can do inductions over
+ the ''input'' (inductively defined assertions)\pause\medskip
+
+ \item Suppose @{text "right_until_zero"}:\bigskip
+
+ \begin{center}
+ \begin{tikzpicture}[scale=1]
+
+ \draw[very thick] (-0.25,0) -- ( 8.25,0);
+ \draw[very thick] (-0.25,0.5) -- ( 8.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[very thick] ( 2.75,0) -- ( 2.75,0.5);
+ \draw[very thick] ( 3.25,0) -- ( 3.25,0.5);
+ \draw[very thick] ( 3.75,0) -- ( 3.75,0.5);
+ \draw[very thick] ( 4.25,0) -- ( 4.25,0.5);
+ \draw[very thick] ( 4.75,0) -- ( 4.75,0.5);
+ \draw[very thick] ( 5.25,0) -- ( 5.25,0.5);
+ \draw[very thick] ( 5.75,0) -- ( 5.75,0.5);
+ \draw[very thick] ( 6.25,0) -- ( 6.25,0.5);
+ \draw[very thick] ( 6.75,0) -- ( 6.75,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);
+ \draw[fill] ( 1.35,0.1) rectangle (1.65,0.4);
+ \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4);
+ \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4);
+ \draw[fill] ( 3.35,0.1) rectangle (3.65,0.4);
+ \draw[fill] ( 3.85,0.1) rectangle (4.15,0.4);
+ \draw[fill] ( 4.35,0.1) rectangle (4.65,0.4);
+ \draw[fill] ( 4.85,0.1) rectangle (5.15,0.4);
+ \draw[fill] ( 5.35,0.1) rectangle (5.65,0.4);
+ \draw[fill] ( 5.85,0.1) rectangle (6.15,0.4);
+
+ \path (2.75,0) edge [decorate,decoration={brace,amplitude=14pt}, thick] node[below=8pt]
+ {\small\textcolor{gray}{@{text "ones u v"}}} (-0.25,0);
+
+ \end{tikzpicture}
+ \end{center}
+
+ \begin{center}
+ @{text "\<lbrace> st i \<star> hd u \<star> zero (v + 1) \<star> ones u v \<rbrace>"}\\
+ @{text "i:[right_until_zero]:j"}\\
+ @{text "\<lbrace> st j \<star> hd (v + 1) \<star> zero (v + 1) \<star> ones u v \<rbrace>"}\\
+ \end{center}
+ \end{itemize}
+
+ \begin{textblock}{3}(11,10)
+ \begin{tikzpicture}
+ \only<2>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}
+ \end{tikzpicture}
+ \end{textblock}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -917,9 +1194,10 @@
\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
+ of the input (e.g.~how many @{text "0"}s/@{text "1"}s are on the tape)
- \item these macros allow us to completely get rid of register machines
+ \item no termination measures are needed
+
\end{itemize}
@@ -931,6 +1209,58 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
+ \frametitle{Register Machines}%
+
+ \begin{itemize}
+ \item We could also use Jensen's et al work to give
+ a more appropriate \alert{view} on register machines
+
+ \begin{center}
+ @{text "\<lbrace>p\<rbrace> i:[rm_c]:j \<lbrace>q\<rbrace>"}
+ \end{center}\bigskip
+ \end{itemize}
+
+ \small
+ \begin{itemize}
+ \item Rule for @{text "Inc"}
+
+ \begin{tabular}{rl}
+ @{text "RM."} & @{text "\<lbrace> pc i \<star> m a v \<rbrace>"} \\
+ & @{text "i:[ Inc a ]:j"} \\
+ & @{text "\<lbrace> pc j \<star> m a (Suc v)\<rbrace>"}
+ \end{tabular}
+ \item Rules for @{text "Dec"}
+ \begin{tabular}{c c}
+ \begin{tabular}{r l}
+ @{text "RM."} & @{text "\<lbrace>(pc i \<star> m a (Suc v))\<rbrace>"} \\
+ & @{text "i :[ Dec a e ]: j"} \\
+ & @{text "\<lbrace>pc j \<star> m a v\<rbrace>"}
+ \end{tabular} &
+ \begin{tabular}{r l}
+ @{text "RM."} & @{text "\<lbrace> pc i \<star> m a 0 \<rbrace>"} \\
+ & @{text "i:[ Dec a e ]:j"} \\
+ & @{text "\<lbrace> pc e \<star> m a 0 \<rbrace>"}
+ \end{tabular}
+ \end{tabular}
+ %\item Rule for @{text "Goto"}
+ %
+ % \begin{tabular}{r l}
+ % @{text "RM."} & @{text "\<lbrace> pc i \<rbrace>"} \\
+ % &@{text "i:[ (Goto e) ]:j"} \\
+ % &@{text "\<lbrace> pc e \<rbrace>"}
+ % \end{tabular}
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
\frametitle{Conclusion}%
\begin{itemize}