702 \begin{frame}[c] |
708 \begin{frame}[c] |
703 \frametitle{Midway Conclusion}% |
709 \frametitle{Midway Conclusion}% |
704 |
710 |
705 \begin{itemize} |
711 \begin{itemize} |
706 \item feels awfully like reasoning about machine code |
712 \item feels awfully like reasoning about machine code |
707 \item compositional constructions / reasoning |
713 \item compositional constructions / reasoning not frictionless |
708 \item sizes |
714 \item sizes |
709 |
715 |
710 \end{itemize} |
716 \begin{center} |
711 |
717 \begin{tabular}{ll} |
712 \end{frame}} |
718 & sizes:\smallskip\\ |
713 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
719 UF & 140843 constructors\\ |
714 *} |
720 Reg.~Mach.~ & @{text 2} Mio instructions\\ |
715 |
721 UTM & @{text 38} Mio states\\ |
716 |
722 \end{tabular} |
717 text_raw {* |
723 \end{center}\pause |
718 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
724 |
719 \mode<presentation>{ |
725 \item an observation: our treatment of recursive functions is a mini-version |
720 \begin{frame}[c] |
726 of the work by\\ Myreen \& Owens about deeply embedding HOL |
721 \frametitle{Recursive Functions}% |
727 \end{itemize} |
722 |
728 |
723 \begin{itemize} |
729 \only<1>{ |
724 \item addition, multiplication, \ldots |
730 \begin{textblock}{4}(2,13.9) |
725 \item logical operations, quantifiers\ldots |
731 \begin{tikzpicture} |
726 \item coding of numbers (Cantor encoding) |
732 \draw (0,0) node {\small\begin{tabular}{l}$^\star$old version: |
727 \item UF\pause\bigskip |
733 RM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}}; |
728 |
734 \end{tikzpicture} |
729 \item Recursive Functions $\Rightarrow$ Register Machines |
735 \end{textblock}} |
730 \item Register Machines $\Rightarrow$ Turing Machines |
736 |
731 \end{itemize} |
737 \end{frame}} |
732 |
738 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
733 \end{frame}} |
739 *} |
734 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
740 |
735 *} |
|
736 |
|
737 text_raw {* |
|
738 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
739 \mode<presentation>{ |
|
740 \begin{frame}[c] |
|
741 \frametitle{Sizes}% |
|
742 |
|
743 \begin{itemize} |
|
744 \item UF (size: @{text 140843}) |
|
745 \item Register Machine (size: @{text 2} Mio instructions) |
|
746 \item UTM (size: @{text 38} Mio states) |
|
747 \end{itemize}\bigskip\bigskip |
|
748 |
|
749 \small |
|
750 old version: RM (@{text 12} Mio) UTM (@{text 112} Mio) |
|
751 \end{frame}} |
|
752 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
753 *} |
|
754 |
741 |
755 text_raw {* |
742 text_raw {* |
756 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
743 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
757 \mode<presentation>{ |
744 \mode<presentation>{ |
758 \begin{frame}[c] |
745 \begin{frame}[c] |