# HG changeset patch # User Christian Urban # Date 1380810543 -3600 # Node ID 5c283ecefda6899ef41a79df0163325ec363329f # Parent 15b8fc34cb082fcf9c01499aa08e890a5c8eea51 added slides diff -r 15b8fc34cb08 -r 5c283ecefda6 ROOT --- a/ROOT Wed Oct 02 13:17:32 2013 +0100 +++ b/ROOT Thu Oct 03 15:29:03 2013 +0100 @@ -18,3 +18,7 @@ theories "Paper" +session Slides6 in "Slides" = Myhill + + options [document = pdf, document_output= "..", document_variants = "slides6"] + theories + "Slides6" \ No newline at end of file diff -r 15b8fc34cb08 -r 5c283ecefda6 Slides/Slides6.thy --- a/Slides/Slides6.thy Wed Oct 02 13:17:32 2013 +0100 +++ b/Slides/Slides6.thy Thu Oct 03 15:29:03 2013 +0100 @@ -1,5 +1,5 @@ (*<*) -theory Slides5 +theory Slides6 imports "~~/src/HOL/Library/LaTeXsugar" begin @@ -11,7 +11,7 @@ text_raw {* - \renewcommand{\slidecaption}{London, 29 August 2012} + \renewcommand{\slidecaption}{London, 3 October 2013} \newcommand{\bl}[1]{\textcolor{blue}{#1}} \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt] \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};} @@ -21,8 +21,9 @@ \frametitle{% \begin{tabular}{@ {}c@ {}} \\[-3mm] - \LARGE The Myhill-Nerode Theorem\\[-3mm] - \LARGE in a Theorem Prover\\[0mm] + \Large A Formalisation of the\\[-1mm] + \Large Myhill-Nerode Theorem using\\[-1mm] + \Large Regular Expressions only \end{tabular}} \begin{center} @@ -35,11 +36,6 @@ University of Science and Technology in Nanjing \end{center} - \only<2->{ - \begin{textblock}{6}(9,5.3) - \alert{\bf Isabelle/HOL} - \end{textblock}} - \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -52,20 +48,15 @@ \mbox{}\\[2mm] \begin{itemize} - \item my background is in - \begin{itemize} - \item \normalsize programming languages and theorem provers - \item \normalsize develop Nominal Isabelle - \end{itemize}\bigskip\bigskip\bigskip\bigskip\bigskip + \item my background is in: + \begin{itemize} + \item \normalsize programming languages and + \item \normalsize theorem provers + \end{itemize}\medskip - \item<1->to formalise and mechanically check proofs from - programming language research, TCS \textcolor{gray}{and OS}\bigskip - - \item<2->we found out that the variable convention can lead to - faulty proofs\ldots + \item \normalsize develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{} \end{itemize} - \onslide<2->{ \begin{center} \begin{block}{} \color{gray} @@ -73,145 +64,22 @@ {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] If $M_1,\ldots,M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables - are chosen to be different from the free variables.\hfill Henk Barendregt + are chosen to be different from the free variables.\hfill ---Henk Barendregt \end{block} - \end{center}} - - - \only<1->{ - \begin{textblock}{6}(10.9,3.5) - \includegraphics[scale=0.23]{isabelle1.png} - \end{textblock}} - - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{} + \end{center}\pause - \begin{tabular}{c@ {\hspace{2mm}}c} - \\[6mm] - \begin{tabular}{c} - \includegraphics[scale=0.11]{harper.jpg}\\[-2mm] - {\footnotesize Bob Harper}\\[-2.5mm] - {\footnotesize (CMU)} - \end{tabular} - \begin{tabular}{c} - \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm] - {\footnotesize Frank Pfenning}\\[-2.5mm] - {\footnotesize (CMU)} - \end{tabular} & + \mbox{}\\[-19mm]\mbox{} - \begin{tabular}{p{6cm}} - \raggedright - \color{gray}{published a proof on LF in\\ {\bf ACM Transactions on Computational Logic}, 2005, - $\sim$31pp} - \end{tabular}\\ - - \pause - \\[0mm] - - \begin{tabular}{c} - \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] - {\footnotesize Andrew Appel}\\[-2.5mm] - {\footnotesize (Princeton)} - \end{tabular} & - - \begin{tabular}{p{6cm}} - \raggedright - \color{gray}{relied on their proof in a\\ {\bf security} critical application\\ (proof-carrying code)} - \end{tabular} - \end{tabular} - - + \begin{itemize} + \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning + about LF (and fixed it in three ways) + \end{itemize} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} - -text {* - \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex] - \tikzstyle{node1}=[rectangle, minimum size=10mm, 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{ - \begin{frame}<2->[squeeze] - \frametitle{} - - \begin{columns} - - \begin{column}{0.8\textwidth} - \begin{textblock}{0}(1,2) - - \begin{tikzpicture} - \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm] - { \&[-10mm] - \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \& - \node (proof1) [node1] {\large Proof}; \& - \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\ - - \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \& - \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \& - \onslide<4->{\node (proof2) [node1] {\large Proof};} \& - \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\ - - \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \& - \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \& - \onslide<5->{\node (proof3) [node1] {\large Proof};} \& - \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\ - - \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \& - \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \& - \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \& - \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\ - }; - - \draw[->,black!50,line width=2mm] (proof1) -- (def1); - \draw[->,black!50,line width=2mm] (proof1) -- (alg1); - - \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);} - \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);} - - \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);} - \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);} - - \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);} - \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);} - - \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} - \end{tikzpicture} - - \end{textblock} - \end{column} - \end{columns} - - - \begin{textblock}{3}(12,3.6) - \onslide<4->{ - \begin{tikzpicture} - \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h}; - \end{tikzpicture}} - \end{textblock} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -219,54 +87,18 @@ \frametitle{} \begin{itemize} - \item I also found fixable errors in my Ph.D.-thesis about cut-elimination + \item found also fixable errors in my Ph.D.-thesis about cut-elimination (examined by Henk Barendregt and Andy Pitts)\bigskip - \item found flaws in a proof about a classic OS scheduling algorithm - --- helped us to implement\\ it correctly and ef$\!$ficiently\\ - {\small\textcolor{gray}{(the existing literature ``proved'' - correct an incorrect algorithm; used in the Mars Pathfinder mission)}} - \end{itemize}\bigskip\bigskip\pause - - - {\bf Conclusion:}\smallskip - - Pencil-and-paper proofs in TCS are not foolproof, - not even expertproof. - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \small Scott Aaronson (Berkeley/MIT):\\[-7mm]\mbox{} - \begin{center} - \begin{block}{} - \color{gray} - \small - ``I still remember having to grade hundreds of exams where the - students started out by assuming what had to be proved, or filled - page after page with gibberish in the hope that, somewhere in the - mess, they might accidentally have said something - correct. \ldots{}innumerable examples of ``parrot proofs'' --- - NP-completeness reductions done in the wrong direction, arguments - that look more like LSD trips than coherent chains of logic \ldots{}'' - \end{block} - \end{center}\pause + \item formalised a classic OS scheduling algorithm (priority inversion + protocol) + \begin{itemize} + \item original algorithm was incorrect even being proved correct (with `pencil-and-paper') + \item helped us to implement this algorithm correctly and efficiently\\ + \end{itemize}\bigskip\pause - \begin{tabular}{@ {}c@ {}} - Tobias Nipkow calls this the ``London Underground Phenomenon'': - \end{tabular} - - \begin{center} - \begin{tabular}{ccc} - students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs - \end{tabular} - \end{center} + \item used Isabelle to prove properties about access controls and OSes + \end{itemize} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -281,7 +113,7 @@ \begin{textblock}{12.9}(1.5,2.0) \begin{block}{} \begin{minipage}{12.4cm}\raggedright - \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} with + \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} theorem\\ provers (especially for inductions). \end{minipage} \end{block} @@ -310,12 +142,12 @@ \begin{textblock}{6}(2,4) \begin{tabular}{@ {}rrl} - \bl{r} & \bl{$::=$} & \bl{$\varnothing$}\\ - & \bl{$\mid$} & \bl{[]}\\ - & \bl{$\mid$} & \bl{c}\\ - & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\ - & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\ - & \bl{$\mid$} & \bl{r$^*$}\\ + \bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\ + & \bl{$\mid$} & \bl{$[]$}\\ + & \bl{$\mid$} & \bl{$c$}\\ + & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\ + & \bl{$\mid$} & \bl{$r_1 + r_2$}\\ + & \bl{$\mid$} & \bl{$r^*$}\\ \end{tabular} \end{textblock} @@ -327,75 +159,226 @@ \footnotesize Isabelle: \end{textblock} - \begin{textblock}{6}(7,12) - \footnotesize\textcolor{gray}{students have seen them and can be motivated about them} - \end{textblock} - - \end{frame}} + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1->[t] + \begin{frame}<1-5>[t] \mbox{}\\[-2mm] \small \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}} - \bl{nullable ($\varnothing$)} & \bl{$=$} & \bl{false} &\\ - \bl{nullable ([])} & \bl{$=$} & \bl{true} &\\ - \bl{nullable (c)} & \bl{$=$} & \bl{false} &\\ - \bl{nullable (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\ - \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\ - \bl{nullable (r$^*$)} & \bl{$=$} & \bl{true} & \\ + \bl{$nullable(\varnothing)$} & \bl{$=$} & \bl{false} &\\ + \bl{$nullable([])$} & \bl{$=$} & \bl{true} &\\ + \bl{$nullable(c)$} & \bl{$=$} & \bl{false} &\\ + \bl{$nullable(r_1 + r_2)$} & \bl{$=$} & \bl{$nullable(r_1) \vee nullable(r_2)$} & \\ + \bl{$nullable(r_1 \cdot r_2)$} & \bl{$=$} & \bl{$nullable(r_1) \wedge nullable(r_2)$} & \\ + \bl{$nullable(r^*)$} & \bl{$=$} & \bl{true} & \\ \end{tabular}\medskip\pause \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}} - \bl{der c ($\varnothing$)} & \bl{$=$} & \bl{$\varnothing$} & \\ - \bl{der c ([])} & \bl{$=$} & \bl{$\varnothing$} & \\ - \bl{der c (d)} & \bl{$=$} & \bl{if c $=$ d then [] else $\varnothing$} & \\ - \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\ - \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$) + } & \\ - & & \bl{\hspace{3mm}(if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\ - \bl{der c (r$^*$)} & \bl{$=$} & \bl{(der c r) $\cdot$ (r$^*$)} &\smallskip\\\pause + \bl{$der\,c\,(\varnothing)$} & \bl{$=$} & \bl{$\varnothing$} & \\ + \bl{$der\,c\,([])$} & \bl{$=$} & \bl{$\varnothing$} & \\ + \bl{$der\,c\,(d)$} & \bl{$=$} & \bl{if $c = d$ then $[]$ else $\varnothing$} & \\ + \bl{$der\,c\,(r_1 + r_2)$} & \bl{$=$} & \bl{$der\,c\,r_1 + der\,c\,r_2$} & \\ + \bl{$der\,c\,(r_1 \cdot r_2)$} & \bl{$=$} & \bl{if $nullable(r_1)$}\\ + & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ + & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\ + \bl{$der\,c\,(r^*)$} & \bl{$=$} & \bl{$(der\,c\,r) \cdot r^*$} &\smallskip\\\pause - \bl{derivative [] r} & \bl{$=$} & \bl{r} & \\ - \bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\ + \bl{$deriv\,[]\,r$} & \bl{$=$} & \bl{$r$} & \\ + \bl{$deriv\,(c::s)\,r$} & \bl{$=$} & \bl{$deriv\,s\,(der\,c\,r)$} & \\ \end{tabular}\medskip - \bl{matches r s $=$ nullable (derivative s r)} + \bl{$match\,r\,s = nullable (deriv\,s\,r)$} + + \only<4>{ + \begin{textblock}{10.5}(2,5) + \begin{tikzpicture} + \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] +{\normalsize\color{darkgray} + \begin{minipage}{10.5cm} + \begin{center} + a)\;\; \bl{$nullable(r) \Leftrightarrow ""\in {\cal L}(r)$}\medskip + \end{center} + + \begin{center} + b)\;\; \bl{${\cal L}(der\,c\,r) = Der\,c\,({\cal L}(r))$} + \end{center} + + where + \begin{center} + \bl{$Der\,c\,A \dn \{s\,|\, c\!::\!s \in A\}$} + \end{center}\medskip\pause + + \begin{center} + c)\;\; \bl{$match\,r\,s \Leftrightarrow s\in{\cal L}(r)$} + \end{center} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\LARGE Regular Expression Matching\\[-2mm] in Education} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[t] +\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}} + +\mbox{}\\[-13mm] + +\begin{tikzpicture}[y=.2cm, x=.3cm] + %axis + \draw (0,0) -- coordinate (x axis mid) (30,0); + \draw (0,0) -- coordinate (y axis mid) (0,30); + %ticks + \foreach \x in {0,5,...,30} + \draw (\x,1pt) -- (\x,-3pt) + node[anchor=north] {\x}; + \foreach \y in {0,5,...,30} + \draw (1pt,\y) -- (-3pt,\y) + node[anchor=east] {\y}; + %labels + \node[below=0.6cm] at (x axis mid) {\bl{a}s}; + \node[rotate=90, left=1.2cm] at (y axis mid) {secs}; - \begin{itemize} - \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip - \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited - for a first-order version''\medskip\bigskip\bigskip\pause - \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined'' - \bigskip + %plots + \draw[color=blue] plot[mark=*, mark options={fill=white}] + file {re-python.data}; + \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] + file {re-ruby.data}; + + %legend + \begin{scope}[shift={(4,20)}] + \draw[color=blue] (0,0) -- + plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) + node[right]{\small Python}; + \draw[yshift=-\baselineskip, color=brown] (0,0) -- + plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (0.5,0) + node[right]{\small Ruby}; + \end{scope} +\end{tikzpicture} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[t] +\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}} + +\mbox{}\\[-13mm] + +\begin{tabular}{@ {\hspace{-5mm}}l} +\begin{tikzpicture}[y=.2cm, x=.01cm] + %axis + \draw (0,0) -- coordinate (x axis mid) (1000,0); + \draw (0,0) -- coordinate (y axis mid) (0,30); + %ticks + \foreach \x in {0,200,...,1000} + \draw (\x,1pt) -- (\x,-3pt) + node[anchor=north] {\x}; + \foreach \y in {0,5,...,30} + \draw (1pt,\y) -- (-3pt,\y) + node[anchor=east] {\y}; + %labels + \node[below=0.6cm] at (x axis mid) {\bl{a}s}; + \node[rotate=90, left=1.2cm] at (y axis mid) {secs}; - \begin{quote}\small - ``Unfortunately, regular expression derivatives have been lost in the - sands of time, and few computer scientists are aware of them.'' - \end{quote} - \end{itemize} - + %plots + \draw[color=blue] plot[mark=*, mark options={fill=white}] + file {re-python.data}; + \draw[color=green] plot[mark=square*, mark options={fill=white} ] + file {re2c.data}; + \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] + file {re-ruby.data}; + + %legend + \begin{scope}[shift={(100,20)}] + \draw[color=blue] (0,0) -- + plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0) + node[right]{\small Python}; + \draw[yshift=-13, color=brown] (0,0) -- + plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0) + node[right]{\small Ruby}; + \draw[yshift=13, color=green] (0,0) -- + plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0) + node[right]{\small nullable + der}; + \end{scope} +\end{tikzpicture} +\end{tabular} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw{* +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[t] +\frametitle{\begin{tabular}{c}\bl{$(a?\{n\}) \cdot a\{n\}$}\end{tabular}} + +\mbox{}\\[-9mm] - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{tabular}{@ {\hspace{-5mm}}l} +\begin{tikzpicture}[y=.2cm, x=.0008cm] + %axis + \draw (0,0) -- coordinate (x axis mid) (12000,0); + \draw (0,0) -- coordinate (y axis mid) (0,30); + %ticks + \foreach \x in {0,2000,...,12000} + \draw (\x,1pt) -- (\x,-3pt) + node[anchor=north] {\x}; + \foreach \y in {0,5,...,30} + \draw (1pt,\y) -- (-3pt,\y) + node[anchor=east] {\y}; + %labels + \node[below=0.6cm] at (x axis mid) {\bl{a}s}; + \node[rotate=90, left=1.2cm] at (y axis mid) {secs}; + %plots + \draw[color=green] plot[mark=square*, mark options={fill=white} ] + file {re2b.data}; + \draw[color=black] plot[mark=square*, mark options={fill=white} ] + file {re3.data}; + \draw[color=blue] plot[mark=*, mark options={fill=white}] + file {re-python.data}; + \draw[color=brown] plot[mark=pentagon*, mark options={fill=white} ] + file {re-ruby.data}; + + %legend + \begin{scope}[shift={(2000,20)}] + \draw[color=blue] (0,0) -- + plot[mark=*, mark options={fill=white}] (0.25,0) -- (50,0) + node[right]{\small Python}; + \draw[yshift=-13, color=brown] (0,0) -- + plot[mark=pentagon*, mark options={fill=white}] (0.25,0) -- (50,0) + node[right]{\small Ruby}; + \draw[yshift=13, color=green] (0,0) -- + plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0) + node[right]{\small nullable + der}; + \draw[yshift=26, color=black] (0,0) -- + plot[mark=square*, mark options={fill=white}] (0.25,0) -- (50,0) + node[right]{\small nullable + der + simplification}; + \end{scope} +\end{tikzpicture} +\end{tabular} + +\end{frame}} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -479,7 +462,7 @@ \begin{block}{} \medskip \begin{minipage}{14cm}\raggedright - Problems with definition for regularity:\bigskip\\ + Already problems with defining regularity:\bigskip\\ \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip \end{minipage} \end{block} @@ -488,7 +471,7 @@ \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\"}\; state nodes\medskip} - \only<7->{You have to \alert{rename} states!} + \only<7->{You have to \alert{rename} states apart!} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -542,7 +525,7 @@ {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause - Infrastructure for free. But do we lose anything?\medskip\pause + Reasoning infrastructure is for free. But do we lose anything?\medskip\pause \begin{minipage}{1.1\textwidth} \begin{itemize} @@ -572,7 +555,7 @@ \item provides necessary and suf\!ficient conditions\\ for a language being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip - \item key is the equivalence relation:\medskip + \item the key notion is the equivalence relation:\medskip \begin{center} \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A} \end{center} @@ -620,7 +603,7 @@ \begin{tikzpicture} \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm] {@{text "\s\"}$_{\approx_{A}}$}; - \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}}; + \draw (0.9,-1.1) node {\begin{tabular}{l}\;\;an equivalence class\end{tabular}}; \end{tikzpicture} \end{textblock}} @@ -702,7 +685,7 @@ \mode{ \begin{frame}<-1>[c] \frametitle{\begin{tabular}{@ {}l}\LARGE% - Transitions between Eq-Classes\end{tabular}} + Transitions\end{tabular}} \begin{center} \begin{tikzpicture}[scale=3] @@ -1147,30 +1130,31 @@ \textcolor{blue}{% \begin{center} \begin{tabular}{@ {}lc@ {\hspace{3mm}}l@ {}} - der c $\varnothing$ & $\dn$ & $\varnothing$\\ - der c [] & $\dn$ & $\varnothing$\\ - der c d & $\dn$ & if c $=$ d then [] else $\varnothing$\\ - der c ($r_1 + r_2$) & $\dn$ & (der c $r_1$) $+$ (der c $r_2$)\\ - der c ($r^*$) & $\dn$ & (der c $r$) $\cdot$ ($r^*$)\\ - der c ($r_1 \cdot r_2$) & $\dn$ & ((der c $r_1$) $\cdot$ $r_2$) +\\ - & & \hspace{-3mm}(if nullable $r_1$ then der c $r_2$ else $\varnothing$)\\ + $der\,c\,\varnothing$ & $\dn$ & $\varnothing$\\ + $der\,c\,[]$ & $\dn$ & $\varnothing$\\ + $der\,c\,d$ & $\dn$ & if $c = d$ then $[]$ else $\varnothing$\\ + $der\,c\,(r_1 + r_2)$ & $\dn$ & $der\,c\,r_1 + der\,c\,r_2$\\ + $der\,c\,(r^*)$ & $\dn$ & $(der\,c\,r) \cdot r^*$\\ + $der\,c\,(r_1 \cdot r_2)$ & $\dn$ & \bl{if $nullable(r_1)$}\\ + & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ + & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\ \end{tabular} \end{center}}} \only<2->{ - \begin{textblock}{13}(1.5,5.7) + \begin{textblock}{14.1}(1.5,5.7) \begin{block}{} \begin{quote} - \begin{minipage}{13cm}\raggedright + \begin{minipage}{14.1cm}\raggedright\rm derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip \begin{center} - \only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(\text{ders}~x~r) = {\cal{L}}(\text{ders}~y~r) + \only<2>{\mbox{\hspace{-22mm}}\smath{{\cal{L}}(deriv~x~r) = {\cal{L}}(deriv~y~r) \Longleftrightarrow x \approx_{{\cal{L}}(r)} y}} - \only<3>{\mbox{\hspace{-22mm}}\smath{\text{ders}~x~r = \text{ders}~y~r + \only<3>{\mbox{\hspace{-22mm}}\smath{deriv~x~r = deriv~y~r \Longrightarrow x \approx_{{\cal{L}}(r)} y}} \end{center}\bigskip \ - \smath{\text{finite}(\text{ders}~A~r)}, but only modulo ACI + \smath{\text{finite}(deriv~A~r)}, but only modulo ACI \begin{center} \begin{tabular}{@ {\hspace{-10mm}}rcl} @@ -1192,20 +1176,21 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<2>[t] - \frametitle{\LARGE\begin{tabular}{c}Partial Derivatives of RExps\end{tabular}} + \frametitle{\LARGE\begin{tabular}{c}Partial Derivatives\end{tabular}} \only<2>{% \textcolor{blue}{% \begin{center} \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} - pder c $\varnothing$ & $\dn$ & \alert{$\{\}$}\\ - pder c [] & $\dn$ & \alert{$\{\}$}\\ - pder c d & $\dn$ & if c $=$ d then $\{$[]$\}$ else $\{\}$\\ - pder c ($r_1 + r_2$) & $\dn$ & (pder c $r_1$) \alert{$\cup$} (der c $r_2$)\\ - pder c ($r^\star$) & $\dn$ & (pder c $r$) $\cdot$ $r^\star$\\ - pder c ($r_1 \cdot r_2$) & $\dn$ & (pder c $r_1$) $\cdot$ $r_2$ \alert{$\cup$}\\ - & & \hspace{-4mm}if nullable $r_1$ then (pder c $r_2$) else $\varnothing$\\ + $pder\,c\,\varnothing$ & $\dn$ & \alert{$\{\}$}\\ + $pder\,c\,[]$ & $\dn$ & \alert{$\{\}$}\\ + $pder\,c\,d$ & $\dn$ & if $c = d$ then $\{[]\}$ else $\{\}$\\ + $pder\,c\,(r_1 + r_2)$ & $\dn$ & $pder\,c\,r_1 \alert{\cup} pder\,c\,r_2$\\ + $pder\,c\,(r^\star)$ & $\dn$ & $(pder\,c\,r) \cdot r^\star$\\ + $pder\,c\,(r_1 \cdot r_2)$ & $\dn$ & \bl{if $nullable(r_1)$}\\ + & & \bl{then $(pder\,c\,r_1) \cdot r_2 \alert{\cup} pder\, c\, r_2$}\\ + & & \bl{else $(pder\, c\, r_1) \cdot r_2$}\\ \end{tabular} \end{center}}} @@ -1213,7 +1198,7 @@ \begin{textblock}{6}(8.5,2.7) \begin{block}{} \begin{quote} - \begin{minipage}{6cm}\raggedright + \begin{minipage}{6cm}\rm\raggedright \begin{itemize} \item partial derivatives \item by Antimirov~'95 @@ -1237,11 +1222,13 @@ \begin{itemize} - \item \alt<1>{\smath{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}} - {\smath{\underbrace{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}_{R}}} + \item \alt<1>{\smath{\text{$pderiv\,x\,r = pderiv\,y\,r$}}} + {\smath{\underbrace{\text{$pderiv\,x\,r = pderiv\,y\,r$}}_{R}}} refines \textcolor{blue}{$x$ $\approx_{{\cal L}(r)}$ $y$}\\[16mm]\pause \item \smath{\text{finite} (U\!N\!IV /\!/ R)} \bigskip\pause - \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed. + \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.\bigskip\pause + + \item We also gave a direct proof, but not as beautiful. \end{itemize} \only<2->{% @@ -1310,51 +1297,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} - - \begin{center} - \huge\bf\textcolor{gray}{in Nuprl} - \end{center} - - \begin{itemize} - \item Constable, Jackson, Naumov, Uribe\medskip - \item \alert{18 months} for automata theory from Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode) - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} - - \begin{center} - \huge\bf\textcolor{gray}{in Coq} - \end{center} - - \begin{itemize} - \item Filli\^atre, Briais, Braibant and others - \item multi-year effort; a number of results in automata theory, e.g.\medskip - \begin{itemize} - \item Kleene's thm.~by Filli\^atre (\alert{``rather big''}) - \item automata theory by Briais (5400 loc) - \item Braibant ATBR library, including Myhill-Nerode\\ ($>$7000 loc) - \item Mirkin's partial derivative automaton construction (10600 loc) - \end{itemize} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -1364,7 +1306,7 @@ \begin{itemize} \item we have never seen a proof of Myhill-Nerode based on - regular expressions only\smallskip\pause + regular expressions\smallskip\pause \item great source of examples (inductions)\smallskip\pause @@ -1374,9 +1316,24 @@ \item second direction (400 / 390 loc) \end{itemize} - \item I am not saying automata are bad; just formal proofs about - them are quite dif$\!$ficult\pause\bigskip\medskip + \item I am not saying automata are bad; just proofs about + them are quite difficult in theorem provers\bigskip + + \item \small our journal paper has just been accepted in JAR (see webpage) + \end{itemize} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE Future Work} + + \begin{itemize} + \item regular expression sub-matching with derivatives (Martin Sulzmann PPDP'12)\bigskip \item parsing with derivatives of grammars\\ (Matt Might ICFP'11) \end{itemize} @@ -1387,43 +1344,8 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}[c] - \frametitle{\LARGE An Apology} - - \begin{itemize} - \item This should all of course be done co-inductively - \end{itemize} - - \footnotesize - \begin{tabular}{@ {\hspace{4mm}}l} - From: Jasmin Christian Blanchette\\ - To: isabelle-dev@mailbroy.informatik.tu-muenchen.de\\ - Subject: [isabelle-dev] NEWS\\ - Date: \alert{\bf Tue, 28 Aug 2012} 17:40:55 +0200\\ - \\ - * {\bf HOL/Codatatype}: New (co)datatype package with support for mixed,\\ - nested recursion and interesting non-free datatypes.\\ - \\ - * HOL/Ordinals\_and\_Cardinals: Theories of ordinals and cardinals\\ - (supersedes the AFP entry of the same name).\\[2mm] - Kudos to Andrei and Dmitriy!\\ - \\ - Jasmin\\[-1mm] - ------------------------------------\\ - isabelle-dev mailing list\\ - isabelle-dev@in.tum.de\\ - \end{tabular} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ \begin{frame}[b] - \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much!\\[5mm]Questions?}} + \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much\\ for listening!\\[5mm]Questions?}} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff -r 15b8fc34cb08 -r 5c283ecefda6 Slides/document/Screen1.png Binary file Slides/document/Screen1.png has changed diff -r 15b8fc34cb08 -r 5c283ecefda6 Slides/document/beamerthemeplaincu.sty --- a/Slides/document/beamerthemeplaincu.sty Wed Oct 02 13:17:32 2013 +0100 +++ b/Slides/document/beamerthemeplaincu.sty Thu Oct 03 15:29:03 2013 +0100 @@ -1,4 +1,4 @@ -\ProvidesPackage{beamerthemeplaincu}[2003/11/07 ver 0.93] +%%\Providespackage{beamerthemeplainculight}[2003/11/07 ver 0.93] \NeedsTeXFormat{LaTeX2e}[1995/12/01] % Copyright 2003 by Till Tantau . @@ -6,29 +6,44 @@ % This program can be redistributed and/or modified under the terms % of the LaTeX Project Public License Distributed from CTAN % archives in directory macros/latex/base/lppl.txt. - + \newcommand{\slidecaption}{} \mode +\usepackage{fontspec} +\usefonttheme{serif} +\defaultfontfeatures{Ligatures=TeX} +\setromanfont{Hoefler Text} +\setmonofont[Scale=MatchLowercase]{Consolas} +\newfontfamily{\consolas}{Consolas} +\newcommand{\tttext}[1]{{\consolas{#1}}} +%%\setttfont{Lucida Console} +%%\setmainfont[Mapping=tex-text]{Hoefler Text} + +%%\renewcommand\ttdefault{lmtt} + + + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % comic fonts fonts -\DeclareFontFamily{T1}{comic}{}% -\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}% -\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}% -\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}% -\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}% -\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}% -\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}% -\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}% -\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}% -\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}% -\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}% -\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}% -\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}% +%\DeclareFontFamily{T1}{comic}{}% +%\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}% +%\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}% +%\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}% +%\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}% +%\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}% +%\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}% +%\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}% +%\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}% +%\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}% +%\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}% +%\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}% +%\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}% % -\renewcommand{\rmdefault}{comic}% -\renewcommand{\sfdefault}{comic}% +%\renewcommand{\rmdefault}{comic}% +%\renewcommand{\sfdefault}{comic}% \renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one % \DeclareMathVersion{bold}% mathfont needs to be bold @@ -43,35 +58,12 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% % Title page -%\usetitlepagetemplate{ -% \vbox{} -% \vfill -% \begin{centering} -% \Large\structure{\textrm{\textit{{\inserttitle}}}} -% \vskip1em\par -% \normalsize\insertauthor\vskip1em\par -% {\scriptsize\insertinstitute\par}\par\vskip1em -% \insertdate\par\vskip1.5em -% \inserttitlegraphic -% \end{centering} -% \vfill -% } +% Frametitles - % Part page -%\usepartpagetemplate{ -% \begin{centering} -% \Large\structure{\textrm{\textit{\partname~\@Roman\c@part}}} -% \vskip1em\par -% \textrm{\textit{\insertpart}}\par -% \end{centering} -% } - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Frametitles -\setbeamerfont{frametitle}{size={\huge}} -\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}} -\setbeamercolor{frametitle}{fg=gray,bg=white} +\setbeamerfont{frametitle}{size={\LARGE}} +\setbeamerfont{frametitle}{family={\fontspec{Hoefler Text Black}}} +%\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}} +\setbeamercolor{frametitle}{fg=ProcessBlue,bg=white} \setbeamertemplate{frametitle}{% \vskip 2mm % distance from the top margin diff -r 15b8fc34cb08 -r 5c283ecefda6 Slides/document/root.tex --- a/Slides/document/root.tex Wed Oct 02 13:17:32 2013 +0100 +++ b/Slides/document/root.tex Thu Oct 03 15:29:03 2013 +0100 @@ -1,8 +1,9 @@ +\documentclass[dvipsnames,14pt,t]{beamer} \usepackage{beamerthemeplaincu} %%\usepackage{ulem} -\usepackage[T1]{fontenc} +%%\usepackage[T1]{fontenc} \usepackage{proof} -\usepackage[latin1]{inputenc} +%%\usepackage[latin1]{inputenc} \usepackage{isabelle} \usepackage{isabellesym} \usepackage{mathpartir} @@ -17,6 +18,9 @@ \usetikzlibrary{shapes} \usetikzlibrary{shadows} \usetikzlibrary{calc} +\usetikzlibrary{plotmarks} +\usetikzlibrary{positioning} + % Isabelle configuration %%\urlstyle{rm} @@ -48,7 +52,7 @@ \newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}} \renewcommand{\isasymequiv}{$\dn$} \renewcommand{\emptyset}{\varnothing}% nice round empty set -\renewcommand{\Gamma}{\varGamma} +%%\renewcommand{\Gamma}{\varGamma} \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}} \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}} \newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}} @@ -134,6 +138,153 @@ {\renewcommand{\isanewline}{\\}\begin{tabbing}}% {\end{tabbing}} +\begin{filecontents}{re-python.data} +1 0.029 +5 0.029 +10 0.029 +15 0.032 +16 0.042 +17 0.042 +18 0.055 +19 0.084 +20 0.136 +21 0.248 +22 0.464 +23 0.899 +24 1.773 +25 3.505 +26 6.993 +27 14.503 +28 29.307 +#29 58.886 +\end{filecontents} + +\begin{filecontents}{re-ruby.data} +1 0.00006 +2 0.00003 +3 0.00001 +4 0.00001 +5 0.00001 +6 0.00002 +7 0.00002 +8 0.00004 +9 0.00007 +10 0.00013 +11 0.00026 +12 0.00055 +13 0.00106 +14 0.00196 +15 0.00378 +16 0.00764 +17 0.01606 +18 0.03094 +19 0.06508 +20 0.12420 +21 0.25393 +22 0.51449 +23 1.02174 +24 2.05998 +25 4.22514 +26 8.42479 +27 16.88678 +28 34.79653 +\end{filecontents} + +\begin{filecontents}{re1.data} +1 0.00179 +2 0.00011 +3 0.00014 +4 0.00026 +5 0.00050 +6 0.00095 +7 0.00190 +8 0.00287 +9 0.00779 +10 0.01399 +11 0.01894 +12 0.03666 +13 0.07994 +14 0.08944 +15 0.02377 +16 0.07392 +17 0.22798 +18 0.65310 +19 2.11360 +20 6.31606 +21 21.46013 +\end{filecontents} + +\begin{filecontents}{re2a.data} +1 0.00227 +5 0.00027 +10 0.00075 +15 0.00178 +20 0.00102 +25 0.00028 +30 0.00040 +35 0.00052 +40 0.00075 +45 0.00125 +50 0.00112 +55 0.00099 +60 0.00113 +65 0.00137 +70 0.00170 +\end{filecontents} + +\begin{filecontents}{re2c.data} +1 0.00020 +51 0.00080 +101 0.00678 +151 0.01792 +201 0.04815 +251 0.09648 +301 0.23195 +351 0.52646 +401 0.96277 +451 1.57726 +501 2.00166 +551 2.98341 +601 4.81181 +651 6.57054 +701 9.73973 +751 13.25762 +801 14.80760 +851 19.60958 +901 25.43550 +951 31.96038 +\end{filecontents} + +\begin{filecontents}{re3.data} +1 0.001605 +501 0.131066 +1001 0.057885 +1501 0.136875 +2001 0.176238 +2501 0.254363 +3001 0.37262 +3501 0.500946 +4001 0.638384 +4501 0.816605 +5001 1.00491 +5501 1.232505 +6001 1.525672 +6501 1.757502 +7001 2.092784 +7501 2.429224 +8001 2.803037 +8501 3.463045 +9001 3.609 +9501 4.081504 +10001 4.54569 +10501 6.17789 +11001 6.77242 +11501 7.95864 +\end{filecontents} + + + + \begin{document} \input{session} \end{document}