tm: comparison Slides/Slides2.thy

equal deleted inserted replaced

-:acc752cef1e7
+:98b3b769ec9a
 \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 him}
+\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
 \end{textblock}}
 \only<4->{
 \begin{textblock}{4}(4.2,12.4)
 \begin{tikzpicture}
-\draw (0,0) node {\begin{tabular}{l}correct UTM by translation\end{tabular}};
+\draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};
 \end{tikzpicture}
 \end{textblock}}
 \end{frame}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \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 content of @{text R} is non-zero,}\\
+& $\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}
 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), UTM
+\item coding of numbers (Cantor encoding), UF
 \end{itemize}
 \end{itemize}
 \mode<presentation>{
 \begin{frame}[c]
 \frametitle{Copy Turing Machine}%
 \begin{itemize}
-\item TM that copies a number on the input tape\smallskip
+\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$};
 \end{center}\bigskip
 \footnotesize
 \begin{center}
 \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
-\multicolumn{3}{@ {\hspace{-8mm}}l}{\small@{text "copy \<equiv> cbegin ; cloop ; cend"}}\\[4mm]
 \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 "]"}
 \mode<presentation>{
 \begin{frame}[c]
 \frametitle{Hoare Reasoning}%
 \begin{itemize}
-\item reasoning is still quite demanding;\\
+\item reasoning is quite demanding, e.g.~the invariants
-the invariants of the copy-machine:\\[-5mm]\mbox{}
+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@ {}}
 \begin{frame}[c]
 \frametitle{Midway Conclusion}%
 \begin{itemize}
 \item feels awfully like reasoning about machine code
-\item compositional constructions / reasoning not at all frictionless
+\item compositional constructions / reasoning is not at all frictionless
 \item sizes
 \begin{center}
 \begin{tabular}{ll}
 & sizes:\smallskip\\
 \mode<presentation>{
 \begin{frame}[c]
 \frametitle{Better Composability}%
 \begin{itemize}
-\item an idea from Jensen, Benton, Kennedy who looked at X86
+\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}
 \begin{center}
 \large @{text "{P} p {Q}"}
 \end{center}\bigskip\medskip
-\item[@{text "(1)"}] we had to find a termination order proving that @{text p} terminates
+\item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}
-\textcolor{gray}{(not easy)}
-\item[@{text "(2)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy either)}
+\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}
 \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.
+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).
+(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}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

changeset 279	98b3b769ec9a
parent 278	acc752cef1e7
child 280	19a4ac992823