# HG changeset patch # User Christian Urban # Date 1385301844 0 # Node ID b49ff5328a6621088a7135b547370efe2bd02aa2 # Parent 447b433b67facbba191101add9e4515561a03fd8 added slides diff -r 447b433b67fa -r b49ff5328a66 Slides/Slides3.thy --- 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{ @@ -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{ \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{ - \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 \ nat list \ 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{ + \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 "\"} @{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{ @@ -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{ \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{ + \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 "\"}\\ @@ -829,26 +969,90 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \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{ + \begin{frame}[c] + \frametitle{Inc a}% + \begin{center} - \alert{very little opportunity for automation} + \begin{tabular}{@ {\hspace{-10mm}}l} + @{text "Inc a"} @{text "\"} \\ + \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 "\ st i \ hd v \ zero u \ ones (u + 1) v \"}\\ + @{text "i:[left_until_zero]:j"}\\ + @{text "\ st j \ hd u \ zero u \ ones (u + 1) v \"}\\ + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \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 "\ st i \ hd u \ zero (v + 1) \ ones u v \"}\\ + @{text "i:[right_until_zero]:j"}\\ + @{text "\ st j \ hd (v + 1) \ zero (v + 1) \ ones u v \"}\\ + \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{ \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 "\p\ i:[rm_c]:j \q\"} + \end{center}\bigskip + \end{itemize} + + \small + \begin{itemize} + \item Rule for @{text "Inc"} + + \begin{tabular}{rl} + @{text "RM."} & @{text "\ pc i \ m a v \"} \\ + & @{text "i:[ Inc a ]:j"} \\ + & @{text "\ pc j \ m a (Suc v)\"} + \end{tabular} + \item Rules for @{text "Dec"} + \begin{tabular}{c c} + \begin{tabular}{r l} + @{text "RM."} & @{text "\(pc i \ m a (Suc v))\"} \\ + & @{text "i :[ Dec a e ]: j"} \\ + & @{text "\pc j \ m a v\"} + \end{tabular} & + \begin{tabular}{r l} + @{text "RM."} & @{text "\ pc i \ m a 0 \"} \\ + & @{text "i:[ Dec a e ]:j"} \\ + & @{text "\ pc e \ m a 0 \"} + \end{tabular} + \end{tabular} + %\item Rule for @{text "Goto"} + % + % \begin{tabular}{r l} + % @{text "RM."} & @{text "\ pc i \"} \\ + % &@{text "i:[ (Goto e) ]:j"} \\ + % &@{text "\ pc e \"} + % \end{tabular} + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] \frametitle{Conclusion}% \begin{itemize}