# HG changeset patch # User urbanc # Date 1321829630 0 # Node ID 1abf8586ee6b78d407ce8df33d291a8e6d6e04de # Parent f512026d5d6e80c70021cce5a1f16376ee38a055 added slides for a talk in St Andrews diff -r f512026d5d6e -r 1abf8586ee6b IsaMakefile --- a/IsaMakefile Fri Nov 11 23:38:10 2011 +0000 +++ b/IsaMakefile Sun Nov 20 22:53:50 2011 +0000 @@ -26,7 +26,7 @@ cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex cp Slides/generated/root.beamer.pdf Slides/slides.pdf -## Slides +## Slides 1 session11: Slides/ROOT.ML \ Slides/document/root* \ @@ -38,6 +38,17 @@ cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex cp Slides/generated/root.beamer.pdf Slides/slides1.pdf +## Slides 2 + +session22: Slides/ROOT.ML \ + Slides/document/root* \ + Slides/Slides2.thy + @$(USEDIR) -D generated -f ROOT2.ML HOL Slides + +slides2: session22 + rm -f Slides/generated/*.aux # otherwise latex will fall over + cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex + cp Slides/generated/root.beamer.pdf Slides/slides2.pdf ## long paper diff -r f512026d5d6e -r 1abf8586ee6b Journal/Paper.thy --- a/Journal/Paper.thy Fri Nov 11 23:38:10 2011 +0000 +++ b/Journal/Paper.thy Sun Nov 20 22:53:50 2011 +0000 @@ -413,7 +413,7 @@ \end{dfntn} \noindent - And then `forget' automata. + And then `forget' automata completely. The reason is that regular expressions, unlike graphs, matrices and functions, can be easily defined as an inductive datatype. A reasoning infrastructure (like induction and recursion) comes for free in @@ -2114,9 +2114,9 @@ @{term "Deriv_lang B A"} is regular. Even more surprising is the fact that for \emph{every} language @{text A}, the language - consisting of all substrings of @{text A} is regular \cite{Haines69} (see also + consisting of all (scattered) substrings of @{text A} is regular \cite{Haines69} (see also \cite{Shallit08, Gasarch09}). - A \emph{substring} can be obtained + A \emph{(scattered) substring} can be obtained by striking out zero or more characters from a string. This can be defined inductively in Isabelle/HOL by the following three rules: diff -r f512026d5d6e -r 1abf8586ee6b Slides/ROOT2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/ROOT2.ML Sun Nov 20 22:53:50 2011 +0000 @@ -0,0 +1,5 @@ +(*show_question_marks := false;*) + +no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; +quick_and_dirty := true; +use_thy "Slides2" \ No newline at end of file diff -r f512026d5d6e -r 1abf8586ee6b Slides/Slides2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/Slides2.thy Sun Nov 20 22:53:50 2011 +0000 @@ -0,0 +1,869 @@ +(*<*) +theory Slides2 +imports "~~/src/HOL/Library/LaTeXsugar" +begin + +notation (latex output) + set ("_") and + Cons ("_::/_" [66,65] 65) + +(*>*) + + +text_raw {* + %\renewcommand{\slidecaption}{Cambridge, 9 November 2010} + %\renewcommand{\slidecaption}{Nijmegen, 25 August 2011} + \renewcommand{\slidecaption}{St Andrews, 19 November 2011} + \newcommand{\bl}[1]{#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}};} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame} + \frametitle{% + \begin{tabular}{@ {}c@ {}} + \LARGE Formalising\\[-3mm] + \LARGE Regular Language Theory\\[-3mm] + \LARGE with Regular Expressions,\\[-3mm] + \LARGE \alert<2>{Only}\\[0mm] + \end{tabular}} + + \begin{center} + Christian Urban\\ + \small King's College London + \end{center}\bigskip + + \begin{center} + \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA + University of Science and Technology in Nanjing + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{} + + \includegraphics[scale=0.5]{roy.jpg}\medskip + + Roy intertwined with my scientific life on many occasions, most + notably:\bigskip + + \begin{itemize} + \item he admitted me for M.Phil.~in St Andrews and\\ + made me like theory\smallskip + \item sent me to Cambridge for Ph.D.\bigskip + \item made me appreciate precision in proofs + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{} + + \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} & + + \begin{tabular}{p{6cm}} + \raggedright + \color{gray}{published a proof 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} + \end{tabular} + \end{tabular}\medskip\pause + + \small + \begin{minipage}{1.0\textwidth} + (I also found an {\bf error} in my Ph.D.-thesis about cut-elimination + examined by Henk Barendregt and Andy Pitts.) + \end{minipage} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} + \mbox{}\\[-15mm]\mbox{} + + \begin{center} + \huge\bf\textcolor{gray}{in Theorem Provers}\\ + \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots} + \end{center} + + \begin{itemize} + \item automata @{text "\"} graphs, matrices, functions + \item<2-> combining automata/graphs + + \onslide<2->{ + \begin{center} + \begin{tabular}{ccc} + \begin{tikzpicture}[scale=1] + %\draw[step=2mm] (-1,-1) grid (1,1); + + \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3); + \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3); + + \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + + \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + + \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + + \draw (-0.6,0.0) node {\small$A_1$}; + \draw ( 0.6,0.0) node {\small$A_2$}; + \end{tikzpicture}} + + & + + \onslide<3->{\raisebox{1.1mm}{\bf\Large$\;\Rightarrow\,$}} + + & + + \onslide<3->{\begin{tikzpicture}[scale=1] + %\draw[step=2mm] (-1,-1) grid (1,1); + + \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3); + \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3); + + \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + + \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + + \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {}; + + \draw (C) to [red, very thick, bend left=45] (B); + \draw (D) to [red, very thick, bend right=45] (B); + + \draw (-0.6,0.0) node {\small$A_1$}; + \draw ( 0.6,0.0) node {\small$A_2$}; + \end{tikzpicture}} + + \end{tabular} + \end{center}\medskip + + \only<4-5>{ + \begin{tabular}{@ {\hspace{-5mm}}l@ {}} + disjoint union:\\[2mm] + \smath{A_1\uplus A_2 \dn \{(1, x)\,|\, x \in A_1\} \,\cup\, \{(2, y)\,|\, y \in A_2\}} + \end{tabular}} + \end{itemize} + + \only<5>{ + \begin{textblock}{13.9}(0.7,7.7) + \begin{block}{} + \medskip + \begin{minipage}{14cm}\raggedright + Problems with definition for regularity:\bigskip\\ + \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip + \end{minipage} + \end{block} + \end{textblock}} + \medskip + + \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\"}\; state nodes\medskip} + + \only<7->{You have to \alert{rename} states!} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}} + \mbox{}\\[-15mm]\mbox{} + + \begin{center} + \huge\bf\textcolor{gray}{in Theorem Provers}\\ + \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots} + \end{center} + + \begin{itemize} + \item Kozen's ``paper'' proof of Myhill-Nerode:\\ + \hspace{2cm}requires absence of \alert{inaccessible states} + \end{itemize}\bigskip\bigskip + + \begin{center} + \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A} + \end{center} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{} + \mbox{}\\[25mm]\mbox{} + + \begin{textblock}{13.9}(0.7,1.2) + \begin{block}{} + \begin{minipage}{13.4cm}\raggedright + {\bf Definition:}\smallskip\\ + + A language \smath{A} is \alert{regular}, provided there exists a\\ + \alert{regular expression} that matches all strings of \smath{A}. + \end{minipage} + \end{block} + \end{textblock}\pause + + {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause + + Infrastructure for free. But do we lose anything?\medskip\pause + + \begin{minipage}{1.1\textwidth} + \begin{itemize} + \item pumping lemma\pause + \item closure under complementation\pause + \item \only<6>{regular expression matching}% + \only<7->{\sout{regular expression matching} + {\footnotesize(@{text "\"}Brozowski'64, Owens et al '09)}} + \item<8-> most textbooks are about automata + \end{itemize} + \end{minipage} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE The Myhill-Nerode Theorem} + + \begin{itemize} + \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 + \begin{center} + \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A} + \end{center} + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE The Myhill-Nerode Theorem} + + \begin{center} + \only<1>{% + \begin{tikzpicture}[scale=3] + \draw[very thick] (0.5,0.5) circle (.6cm); + \end{tikzpicture}}% + \only<2->{% + \begin{tikzpicture}[scale=3] + \draw[very thick] (0.5,0.5) circle (.6cm); + \clip[draw] (0.5,0.5) circle (.6cm); + \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4); + \end{tikzpicture}} + \end{center} + + \begin{itemize} + \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}} + \end{itemize} + + \begin{textblock}{5}(2.1,5.3) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=2cm] + {$U\!N\!IV$}; + \draw (-0.3,-1.1) node {\begin{tabular}{l}set of all\\[-1mm] strings\end{tabular}}; + \end{tikzpicture} + \end{textblock} + + \only<2->{% + \begin{textblock}{5}(9.1,7.2) + \begin{tikzpicture} + \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm] + {@{text "\x\"}$_{\approx_{A}}$}; + \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}}; + \end{tikzpicture} + \end{textblock}} + + \only<3->{ + \begin{textblock}{11.9}(1.7,3) + \begin{block}{} + \begin{minipage}{11.4cm}\raggedright + Two directions:\medskip\\ + \begin{tabular}{@ {}ll} + 1.)\;finite $\Rightarrow$ regular\\ + \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_A) \Rightarrow \exists r.\;A = {\cal L}(r)}\\[3mm] + 2.)\;regular $\Rightarrow$ finite\\ + \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{{\cal L}(r)})} + \end{tabular} + + \end{minipage} + \end{block} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE Initial and Final {\sout{\textcolor{gray}{States}}}} + + \begin{textblock}{8}(10, 2) + \textcolor{black}{Equivalence Classes} + \end{textblock} + + + \begin{center} + \begin{tikzpicture}[scale=3] + \draw[very thick] (0.5,0.5) circle (.6cm); + \clip[draw] (0.5,0.5) circle (.6cm); + \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4); + \only<2->{\draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);} + \only<3->{\draw[red, fill] (0.2, 0.2) rectangle (0.4, 0.4); + \draw[red, fill] (0.4, 0.8) rectangle (0.6, 1.0); + \draw[red, fill] (0.6, 0.0) rectangle (0.8, 0.2); + \draw[red, fill] (0.8, 0.4) rectangle (1.0, 0.6);} + \end{tikzpicture} + \end{center} + + \begin{itemize} + \item \smath{\text{finals}\,A\,\dn \{[\!|x|\!]_{\approx_{A}}\;|\;x \in A\}} + \smallskip + \item we can prove: \smath{A = \bigcup \text{finals}\,A} + \end{itemize} + + \only<2->{% + \begin{textblock}{5}(2.1,4.6) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=blue,text=white, minimum height=2cm] + {$[] \in X$}; + \end{tikzpicture} + \end{textblock}} + + \only<3->{% + \begin{textblock}{5}(10,7.4) + \begin{tikzpicture} + \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm] + {a final}; + \end{tikzpicture} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<-1>[c] + \frametitle{\begin{tabular}{@ {}l}\LARGE% + Transitions between Eq-Classes\end{tabular}} + + \begin{center} + \begin{tikzpicture}[scale=3] + \draw[very thick] (0.5,0.5) circle (.6cm); + \clip[draw] (0.5,0.5) circle (.6cm); + \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4); + \draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8); + \draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6); + \draw[white] (0.1,0.7) node (X) {$X$}; + \draw[white] (0.9,0.5) node (Y) {$Y$}; + \draw[blue, ->, line width = 2mm, bend left=45] (X) -- (Y); + \node [inner sep=1pt,label=above:\textcolor{blue}{$c$}] at ($ (X)!.5!(Y) $) {}; + \end{tikzpicture} + \end{center} + + \begin{center} + \smath{X \stackrel{c}{\longrightarrow} Y \;\dn\; X ; c \subseteq Y} + \end{center} + + \onslide<8>{ + \begin{tabular}{c} + \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick] + \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] + \node[state,initial] (q_0) {$R_1$}; + \end{tikzpicture} + \end{tabular}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE Systems of Equations} + + Inspired by a method of Brzozowski\;'64:\bigskip\bigskip + + \begin{center} + \begin{tabular}{@ {\hspace{-20mm}}c} + \\[-13mm] + \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick] + \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] + + %\draw[help lines] (0,0) grid (3,2); + + \node[state,initial] (p_0) {$X_1$}; + \node[state,accepting] (p_1) [right of=q_0] {$X_2$}; + + \path[->] (p_0) edge [bend left] node {a} (p_1) + edge [loop above] node {b} () + (p_1) edge [loop above] node {a} () + edge [bend left] node {b} (p_0); + \end{tikzpicture}\\ + \\[-13mm] + \end{tabular} + \end{center} + + \begin{center} + \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l} + & \smath{X_1} & \smath{=} & \smath{X_1;b + X_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\ + & \smath{X_2} & \smath{=} & \smath{X_1;a + X_2;a}\medskip\\ + \end{tabular} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-2,4->[t] + \small + + \begin{center} + \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll} + \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} + & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\ + \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}} + & \onslide<1->{\smath{X_1; a + X_2; a}}\\ + + & & & \onslide<2->{by Arden}\\ + + \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} + & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\ + \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}} + & \only<2->{\smath{X_1; a\cdot a^\star}}\\ + + & & & \onslide<4->{by Arden}\\ + + \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} + & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\ + \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}} + & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\ + + & & & \onslide<5->{by substitution}\\ + + \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} + & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\ + \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}} + & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\ + + & & & \onslide<6->{by Arden}\\ + + \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} + & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ + \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}} + & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\ + + & & & \onslide<7->{by substitution}\\ + + \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} + & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\ + \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}} + & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star + \cdot a\cdot a^\star}}\\ + \end{tabular} + \end{center} + + \only<8->{ + \begin{textblock}{6}(2.5,4) + \begin{block}{} + \begin{minipage}{8cm}\raggedright + + \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm] + \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm] + + %\draw[help lines] (0,0) grid (3,2); + + \node[state,initial] (p_0) {$X_1$}; + \node[state,accepting] (p_1) [right of=q_0] {$X_2$}; + + \path[->] (p_0) edge [bend left] node {a} (p_1) + edge [loop above] node {b} () + (p_1) edge [loop above] node {a} () + edge [bend left] node {b} (p_0); + \end{tikzpicture} + + \end{minipage} + \end{block} + \end{textblock}} + + \only<1,2>{% + \begin{textblock}{3}(0.6,1.2) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<2>{% + \begin{textblock}{3}(0.6,3.6) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<4>{% + \begin{textblock}{3}(0.6,2.9) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<4>{% + \begin{textblock}{3}(0.6,5.3) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<5>{% + \begin{textblock}{3}(1.0,5.6) + \begin{tikzpicture} + \node at (0,0) (A) {}; + \node at (0,1) (B) {}; + \draw[<-, line width=2mm, red] (B) to (A); + \end{tikzpicture} + \end{textblock}} + \only<5,6>{% + \begin{textblock}{3}(0.6,7.7) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<6>{% + \begin{textblock}{3}(0.6,10.1) + \begin{tikzpicture} + \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm] + {\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock}} + \only<7>{% + \begin{textblock}{3}(1.0,10.3) + \begin{tikzpicture} + \node at (0,0) (A) {}; + \node at (0,1) (B) {}; + \draw[->, line width=2mm, red] (B) to (A); + \end{tikzpicture} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE The Other Direction} + + One has to prove + + \begin{center} + \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})} + \end{center} + + by induction on \smath{r}. Not trivial, but after a bit + of thinking, one can find a \alert{refined} relation:\bigskip + + + \begin{center} + \mbox{\begin{tabular}{c@ {\hspace{7mm}}c@ {\hspace{7mm}}c} + \begin{tikzpicture}[scale=1.1] + %Circle + \draw[thick] (0,0) circle (1.1); + \end{tikzpicture} + & + \begin{tikzpicture}[scale=1.1] + %Circle + \draw[thick] (0,0) circle (1.1); + %Main rays + \foreach \a in {0, 90,...,359} + \draw[very thick] (0, 0) -- (\a:1.1); + \foreach \a / \l in {45/1, 135/2, 225/3, 315/4} + \draw (\a: 0.65) node {\small$a_\l$}; + \end{tikzpicture} + & + \begin{tikzpicture}[scale=1.1] + %Circle + \draw[red, thick] (0,0) circle (1.1); + %Main rays + \foreach \a in {0, 45,...,359} + \draw[red, very thick] (0, 0) -- (\a:1.1); + \foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2} + \draw (\a: 0.77) node {\textcolor{red}{\footnotesize$a_{\l}$}}; + \end{tikzpicture}\\ + \small\smath{U\!N\!IV} & + \small\smath{U\!N\!IV /\!/ \approx_{{\cal L}(r)}} & + \small\smath{U\!N\!IV /\!/ \alert{R}} + \end{tabular}} + \end{center} + + \begin{textblock}{5}(9.8,2.6) + \begin{tikzpicture} + \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}}; + \end{tikzpicture} + \end{textblock} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{\LARGE\begin{tabular}{c}Derivatives of RExps\end{tabular}} + + \begin{itemize} + \item introduced by Brozowski~'64 + \item a regular expressions after a character has been parsed\\[-18mm]\mbox{} + \end{itemize} + + \only<1>{% + \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^\star$) & $\dn$ & (der c $r$) $\cdot$ $r^\star$\\ + der c ($r_1 \cdot r_2$) & $\dn$ & if nullable $r_1$\\ + & & then (der c $r_1$) $\cdot$ $r_2$ $+$ (der c $r_2$)\\ + & & else (der c $r_1$) $\cdot$ $r_2$\\ + \end{tabular} + \end{center}}} + \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$ & if nullable $r_1$\\ + & & then (pder c $r_1$) $\cdot$ $r_2$ \alert{$\cup$} (pder c $r_2$)\\ + & & else (pder c $r_1$) $\cdot$ $r_2$\\ + \end{tabular} + \end{center}}} + + \only<2>{ + \begin{textblock}{6}(8.5,4.7) + \begin{block}{} + \begin{quote} + \begin{minipage}{6cm}\raggedright + \begin{itemize} + \item partial derivatives + \item by Antimirov~'95 + \end{itemize} + \end{minipage} + \end{quote} + \end{block} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{\LARGE Partial Derivatives} + + \mbox{}\\[0mm]\mbox{} + + \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}}} + 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. + \end{itemize} + + \only<2->{% + \begin{textblock}{5}(3.9,7.2) + \begin{tikzpicture} + \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}}; + \draw (2.2,0) node {Antimirov '95}; + \end{tikzpicture} + \end{textblock}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[t] + \frametitle{\LARGE What Have We Achieved?} + + \begin{itemize} + \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}} + \medskip\pause + \item regular languages are closed under complementation; this is now easy + \begin{center} + \smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}} + \end{center}\pause\medskip + + \item non-regularity (\smath{a^nb^n})\medskip\pause\pause + + \item take \alert{\bf any} language; build the language of substrings\\ + \pause + + then this language \alert{\bf is} regular\;\; (\smath{a^nb^n} $\Rightarrow$ \smath{a^\star{}b^\star}) + + \end{itemize} + +\only<2>{ +\begin{textblock}{10}(4,14) +\small +\smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A} +\end{textblock}} + +\only<4>{ +\begin{textblock}{5}(2,8.6) +\begin{minipage}{8.8cm} +\begin{block}{} +\begin{minipage}{8.6cm} +If there exists a sufficiently large set \smath{B} (for example infinitely large), +such that + +\begin{center} +\smath{\forall x,y \in B.\; x \not= y \;\Rightarrow\; x \not\approx_{A} y}. +\end{center} + +then \smath{A} is not regular.\hspace{1.3cm}\small(\smath{B \dn \bigcup_n a^n}) +\end{minipage} +\end{block} +\end{minipage} +\end{textblock} +} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{\LARGE Conclusion} + + \begin{itemize} + \item We have never seen a proof of Myhill-Nerode based on + regular expressions.\smallskip\pause + + \item great source of examples (inductions)\smallskip\pause + + \item no need to fight the theorem prover:\\ + \begin{itemize} + \item first direction (790 loc)\\ + \item second direction (400 / 390 loc) + \end{itemize} + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[b] + \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you!\\[5mm]Questions?}} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +(*<*) +end +(*>*) \ No newline at end of file diff -r f512026d5d6e -r 1abf8586ee6b Slides/document/appel.jpg Binary file Slides/document/appel.jpg has changed diff -r f512026d5d6e -r 1abf8586ee6b Slides/document/harper.jpg Binary file Slides/document/harper.jpg has changed diff -r f512026d5d6e -r 1abf8586ee6b Slides/document/pfenning.jpg Binary file Slides/document/pfenning.jpg has changed diff -r f512026d5d6e -r 1abf8586ee6b Slides/document/roy.jpg Binary file Slides/document/roy.jpg has changed diff -r f512026d5d6e -r 1abf8586ee6b Slides/slides.pdf Binary file Slides/slides.pdf has changed diff -r f512026d5d6e -r 1abf8586ee6b Slides/slides1.pdf Binary file Slides/slides1.pdf has changed diff -r f512026d5d6e -r 1abf8586ee6b Slides/slides2.pdf Binary file Slides/slides2.pdf has changed diff -r f512026d5d6e -r 1abf8586ee6b csupp.pdf Binary file csupp.pdf has changed diff -r f512026d5d6e -r 1abf8586ee6b csupp.tex --- a/csupp.tex Fri Nov 11 23:38:10 2011 +0000 +++ b/csupp.tex Sun Nov 20 22:53:50 2011 +0000 @@ -43,7 +43,8 @@ it increasingly clear, that this is not true anymore~\cite{Might11}. And there is a real practical need for new results: for example the future HTML5 Standard abandons a well-defined grammar specification, in favour of a bespoke -parser given as pseudo code. +parser given as pseudo code. Proving any property about this parser is nearly +impossible. This work targets parsers from a certification point of view. Increasingly, parsers are part of certified compilers, like @@ -77,7 +78,7 @@ (CFGs). This extension introduces new regular operators, such as negation and conjunction, on the right-hand side of grammar rules, as well as priority orderings for rules. With these extensions, PEG parsing becomes much -more powerful and more useful in practise. For example disambiguation, formerly expressed by semantic +more powerful and more useful in practice. For example disambiguation, formerly expressed by semantic filters, can now be expressed directly using grammar rules. However, there is a serious limitation of PEGs, which affects potential @@ -93,9 +94,9 @@ parsing. There are also good indications that we can adapt work on Boolean Grammars~\cite{Okhotin04}, which are similar to PEGs and for which the paper~\cite{KountouriotisNR09} gives a fixed-point semantics -to negation operators, but not to the Kleene star. +for negation operators, but not to the Kleene star. -For the parsing algorithm, we might be able to build upon +For our parsing algorithm, we might be able to build upon the classic Cocke-Younger-Kasami (CYK) algorithms~\cite{KountouriotisNR09} and Early~\cite{AycHor02, Earley70} parsers. The defect of CYK algorithms, however,