--- a/Slides/langs.sty Tue Jun 14 12:24:25 2016 +0100
+++ b/Slides/langs.sty Tue Jun 14 12:37:46 2016 +0100
@@ -67,3 +67,28 @@
\makeatother
\lstset{escapeinside={(*@}{@*)}}
+
+
+
+\newcommand\grid[1]{%
+\begin{tikzpicture}[baseline=(char.base)]
+ \path[use as bounding box]
+ (0,0) rectangle (1em,1em);
+ \draw[red!50, fill=red!20]
+ (0,0) rectangle (1em,1em);
+ \node[inner sep=1pt,anchor=base west]
+ (char) at (0em,\gridraiseamount) {#1};
+\end{tikzpicture}}
+\newcommand\gridraiseamount{0.12em}
+
+\makeatletter
+\newcommand\Grid[1]{%
+ \@tfor\z:=#1\do{\grid{\z}}}
+\makeatother
+
+\newcommand\Vspace[1][.3em]{%
+ \mbox{\kern.06em\vrule height.3ex}%
+ \vbox{\hrule width#1}%
+ \hbox{\vrule height.3ex}}
+
+\def\VS{\Vspace[0.6em]}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/proof.sty Tue Jun 14 12:37:46 2016 +0100
@@ -0,0 +1,278 @@
+% proof.sty (Proof Figure Macros)
+%
+% version 3.0 (for both LaTeX 2.09 and LaTeX 2e)
+% Mar 6, 1997
+% Copyright (C) 1990 -- 1997, Makoto Tatsuta (tatsuta@kusm.kyoto-u.ac.jp)
+%
+% This program is free software; you can redistribute it or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either versions 1, or (at your option)
+% any later version.
+%
+% This program is distributed in the hope that it will be useful
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+% GNU General Public License for more details.
+%
+% Usage:
+% In \documentstyle, specify an optional style `proof', say,
+% \documentstyle[proof]{article}.
+%
+% The following macros are available:
+%
+% In all the following macros, all the arguments such as
+% <Lowers> and <Uppers> are processed in math mode.
+%
+% \infer<Lower><Uppers>
+% draws an inference.
+%
+% Use & in <Uppers> to delimit upper formulae.
+% <Uppers> consists more than 0 formulae.
+%
+% \infer returns \hbox{ ... } or \vbox{ ... } and
+% sets \@LeftOffset and \@RightOffset globally.
+%
+% \infer[<Label>]<Lower><Uppers>
+% draws an inference labeled with <Label>.
+%
+% \infer*<Lower><Uppers>
+% draws a many step deduction.
+%
+% \infer*[<Label>]<Lower><Uppers>
+% draws a many step deduction labeled with <Label>.
+%
+% \infer=<Lower><Uppers>
+% draws a double-ruled deduction.
+%
+% \infer=[<Label>]<Lower><Uppers>
+% draws a double-ruled deduction labeled with <Label>.
+%
+% \deduce<Lower><Uppers>
+% draws an inference without a rule.
+%
+% \deduce[<Proof>]<Lower><Uppers>
+% draws a many step deduction with a proof name.
+%
+% Example:
+% If you want to write
+% B C
+% -----
+% A D
+% ----------
+% E
+% use
+% \infer{E}{
+% A
+% &
+% \infer{D}{B & C}
+% }
+%
+
+% Style Parameters
+
+\newdimen\inferLineSkip \inferLineSkip=2pt
+\newdimen\inferLabelSkip \inferLabelSkip=5pt
+\def\inferTabSkip{\quad}
+
+% Variables
+
+\newdimen\@LeftOffset % global
+\newdimen\@RightOffset % global
+\newdimen\@SavedLeftOffset % safe from users
+
+\newdimen\UpperWidth
+\newdimen\LowerWidth
+\newdimen\LowerHeight
+\newdimen\UpperLeftOffset
+\newdimen\UpperRightOffset
+\newdimen\UpperCenter
+\newdimen\LowerCenter
+\newdimen\UpperAdjust
+\newdimen\RuleAdjust
+\newdimen\LowerAdjust
+\newdimen\RuleWidth
+\newdimen\HLabelAdjust
+\newdimen\VLabelAdjust
+\newdimen\WidthAdjust
+
+\newbox\@UpperPart
+\newbox\@LowerPart
+\newbox\@LabelPart
+\newbox\ResultBox
+
+% Flags
+
+\newif\if@inferRule % whether \@infer draws a rule.
+\newif\if@DoubleRule % whether \@infer draws doulbe rules.
+\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
+\newif\if@MathSaved % whether inner math mode where \infer or
+ % \deduce appears.
+
+% Special Fonts
+
+\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
+ \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
+
+% Math Save Macros
+%
+% \@SaveMath is called in the very begining of toplevel macros
+% which are \infer and \deduce.
+% \@RestoreMath is called in the very last before toplevel macros end.
+% Remark \infer and \deduce ends calling \@infer.
+
+\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
+ \relax $\relax \@MathSavedtrue \fi\fi }
+
+\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
+
+% Macros
+
+% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.
+
+\def\@IFnextchar#1#2#3{%
+ \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet
+ \reserved@c\@IFnch}
+\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch
+ \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else
+ \let\reserved@d\reserved@b\fi
+ \fi \reserved@d}
+
+\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
+ \ifx \@tempa \@tempb #2\else #3\fi }
+
+\def\infer{\@SaveMath \@IFnextchar *{\@inferSteps}{\relax
+ \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
+
+\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
+ \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
+ \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferSteps*{\@IFnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
+
+\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
+
+\def\deduce{\@SaveMath \@IFnextchar [{\@deduce{\@empty}}
+ {\@inferRulefalse \@infer[\@empty]}}
+
+% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+
+\def\@deduce#1[#2]#3#4{\@inferRulefalse
+ \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
+
+% \@infer[<Label>]<Lower><Uppers>
+% If \@inferRuletrue, it draws a rule and <Label> is right to
+% a rule. In this case, if \@DoubleRuletrue, it draws
+% double rules.
+%
+% Otherwise, draws no rule and <Label> is right to <Lower>.
+
+\def\@infer[#1]#2#3{\relax
+% Get parameters
+ \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
+ \setbox\@LabelPart=\hbox{$#1$}\relax
+ \setbox\@LowerPart=\hbox{$#2$}\relax
+%
+ \global\@LeftOffset=0pt
+ \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
+ \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
+ \inferTabSkip
+ \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
+ #3\cr}}\relax
+% Here is a little trick.
+% \@ReturnLeftOffsettrue(false) influences on \infer or
+% \deduce placed in ## locally
+% because of \@SaveMath and \@RestoreMath.
+ \UpperLeftOffset=\@LeftOffset
+ \UpperRightOffset=\@RightOffset
+% Calculate Adjustments
+ \LowerWidth=\wd\@LowerPart
+ \LowerHeight=\ht\@LowerPart
+ \LowerCenter=0.5\LowerWidth
+%
+ \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
+ \advance\UpperWidth by -\UpperRightOffset
+ \UpperCenter=\UpperLeftOffset
+ \advance\UpperCenter by 0.5\UpperWidth
+%
+ \ifdim \UpperWidth > \LowerWidth
+ % \UpperCenter > \LowerCenter
+ \UpperAdjust=0pt
+ \RuleAdjust=\UpperLeftOffset
+ \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
+ \RuleWidth=\UpperWidth
+ \global\@LeftOffset=\LowerAdjust
+%
+ \else % \UpperWidth <= \LowerWidth
+ \ifdim \UpperCenter > \LowerCenter
+%
+ \UpperAdjust=0pt
+ \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+ \LowerAdjust=\RuleAdjust
+ \RuleWidth=\LowerWidth
+ \global\@LeftOffset=\LowerAdjust
+%
+ \else % \UpperWidth <= \LowerWidth
+ % \UpperCenter <= \LowerCenter
+%
+ \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+ \RuleAdjust=0pt
+ \LowerAdjust=0pt
+ \RuleWidth=\LowerWidth
+ \global\@LeftOffset=0pt
+%
+ \fi\fi
+% Make a box
+ \if@inferRule
+%
+ \setbox\ResultBox=\vbox{
+ \moveright \UpperAdjust \box\@UpperPart
+ \nointerlineskip \kern\inferLineSkip
+ \if@DoubleRule
+ \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
+ \kern 1pt\hrule width\RuleWidth}\relax
+ \else
+ \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+ \fi
+ \nointerlineskip \kern\inferLineSkip
+ \moveright \LowerAdjust \box\@LowerPart }\relax
+%
+ \@ifEmpty{#1}{}{\relax
+%
+ \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
+ \advance\HLabelAdjust by -\RuleWidth
+ \WidthAdjust=\HLabelAdjust
+ \advance\WidthAdjust by -\inferLabelSkip
+ \advance\WidthAdjust by -\wd\@LabelPart
+ \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
+%
+ \VLabelAdjust=\dp\@LabelPart
+ \advance\VLabelAdjust by -\ht\@LabelPart
+ \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
+ \advance\VLabelAdjust by \inferLineSkip
+%
+ \setbox\ResultBox=\hbox{\box\ResultBox
+ \kern -\HLabelAdjust \kern\inferLabelSkip
+ \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
+%
+ }\relax % end @ifEmpty
+%
+ \else % \@inferRulefalse
+%
+ \setbox\ResultBox=\vbox{
+ \moveright \UpperAdjust \box\@UpperPart
+ \nointerlineskip \kern\inferLineSkip
+ \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
+ \@ifEmpty{#1}{}{\relax
+ \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
+ \fi
+%
+ \global\@RightOffset=\wd\ResultBox
+ \global\advance\@RightOffset by -\@LeftOffset
+ \global\advance\@RightOffset by -\LowerWidth
+ \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
+%
+ \box\ResultBox
+ \@RestoreMath
+}
Binary file Slides/slides01.pdf has changed
--- a/Slides/slides01.tex Tue Jun 14 12:24:25 2016 +0100
+++ b/Slides/slides01.tex Tue Jun 14 12:37:46 2016 +0100
@@ -2,7 +2,6 @@
\usepackage{slides}
\usepackage{langs}
\usepackage{graph}
-%\usepackage{grammar}
\usepackage{soul}
\usepackage{data}
\usepackage{proof}
@@ -11,31 +10,6 @@
\renewcommand{\slidecaption}{Canterbury, 22.2.2016}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
-\newcommand\grid[1]{%
-\begin{tikzpicture}[baseline=(char.base)]
- \path[use as bounding box]
- (0,0) rectangle (1em,1em);
- \draw[red!50, fill=red!20]
- (0,0) rectangle (1em,1em);
- \node[inner sep=1pt,anchor=base west]
- (char) at (0em,\gridraiseamount) {#1};
-\end{tikzpicture}}
-\newcommand\gridraiseamount{0.12em}
-
-\makeatletter
-\newcommand\Grid[1]{%
- \@tfor\z:=#1\do{\grid{\z}}}
-\makeatother
-
-\newcommand\Vspace[1][.3em]{%
- \mbox{\kern.06em\vrule height.3ex}%
- \vbox{\hrule width#1}%
- \hbox{\vrule height.3ex}}
-
-\def\VS{\Vspace[0.6em]}
-
-
-
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
Binary file Slides/slides03.pdf has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/slides03.tex Tue Jun 14 12:37:46 2016 +0100
@@ -0,0 +1,494 @@
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{slides}
+\usepackage{langs}
+\usepackage{graph}
+\usepackage{data}
+\usepackage{proof}
+
+% beamer stuff
+\renewcommand{\slidecaption}{ITP ????}
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+
+
+\begin{document}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\
+ \Large POSIX Lexing with Derivatives\\[-1.5mm]
+ \Large of Regular Expressions\\
+ \Large (Proof Pearl)\\[-1mm]
+ \end{tabular}}\bigskip\bigskip\bigskip
+
+ \normalsize
+ \begin{center}
+ \begin{tabular}{c}
+ \small Fahad Ausaf\\
+ \small King's College London\\
+ \\
+ \small joint work with Roy Dyckhoff and Christian Urban
+ \end{tabular}
+ \end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Regular Expressions}
+
+
+\begin{textblock}{6}(2,5)
+ \begin{tabular}{rrl@ {\hspace{13mm}}l}
+ \bl{$r$} & \bl{$::=$} & \bl{$\varnothing$} & null\\
+ & \bl{$\mid$} & \bl{$\epsilon$} & empty string\\
+ & \bl{$\mid$} & \bl{$c$} & character\\
+ & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
+ & \bl{$\mid$} & \bl{$r_1 + r_2$} & alternative / choice\\
+ & \bl{$\mid$} & \bl{$r^*$} & star (zero or more)\\
+ \end{tabular}
+ \end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{The Derivative of a Rexp}
+
+\large
+If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular
+expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip
+
+\small
+\bl{$der\,c\,r$} gives the answer, Brzozowski (1964), Owens (2005)
+``\ldots have been lost in the sands of time\ldots''
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Correctness}
+
+It is a relative easy exercise in a theorem prover:
+
+\begin{center}
+\bl{$matches(r, s)$} if and only if \bl{$s \in L(r)$}
+\end{center}\bigskip
+
+\small
+where \bl{$matches(r, s) \dn nullable(ders(r, s))$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{POSIX Regex Matching}
+
+Two rules:
+
+\begin{itemize}
+\item Longest match rule (``maximal munch rule''): The
+longest initial substring matched by any regular expression
+is taken as the next token.
+
+\begin{center}
+\bl{$\texttt{\Grid{iffoo\VS bla}}$}
+\end{center}\medskip
+
+\item Rule priority:
+For a particular longest initial substring, the first regular
+expression that can match determines the token.
+
+\begin{center}
+\bl{$\texttt{\Grid{if\VS bla}}$}
+\end{center}
+\end{itemize}\bigskip\pause
+
+\small
+\hfill Kuklewicz: most POSIX matchers are buggy\\
+\footnotesize
+\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{POSIX Regex Matching}
+
+\begin{itemize}
+
+\item Sulzmann \& Lu came up with a beautiful
+idea for how to extend the simple regular expression
+matcher to POSIX matching/lexing (FLOPS 2014)\bigskip\bigskip
+
+\begin{tabular}{@{\hspace{4cm}}c@{}}
+ \includegraphics[scale=0.20]{pics/sulzmann.jpg}\\[-2mm]
+ \hspace{0cm}\footnotesize Martin Sulzmann
+\end{tabular}\bigskip\bigskip
+
+\item the idea: define an inverse operation to the derivatives
+\end{itemize}
+
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Regexes and Values}
+
+Regular expressions and their corresponding values
+(for \emph{how} a regular expression matched a string):
+
+\begin{center}
+\begin{columns}
+\begin{column}{3cm}
+\begin{tabular}{@{}rrl@{}}
+ \bl{$r$} & \bl{$::=$} & \bl{$\varnothing$}\\
+ & \bl{$\mid$} & \bl{$\epsilon$} \\
+ & \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{column}
+\begin{column}{3cm}
+\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
+ \bl{$v$} & \bl{$::=$} & \\
+ & & \bl{$Empty$} \\
+ & \bl{$\mid$} & \bl{$Char(c)$} \\
+ & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
+ & \bl{$\mid$} & \bl{$Left(v)$} \\
+ & \bl{$\mid$} & \bl{$Right(v)$} \\
+ & \bl{$\mid$} & \bl{$[]$} \\
+ & \bl{$\mid$} & \bl{$[v_1,\ldots\,v_n]$} \\
+ \end{tabular}
+\end{column}
+\end{columns}
+\end{center}\pause
+
+There is also a notion of a string behind a value: \bl{$|v|$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Sulzmann \& Lu Matcher}
+
+We want to match the string \bl{$abc$} using \bl{$r_1$}:
+
+\begin{center}
+\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
+\node (r1) {\bl{$r_1$}};
+\node (r2) [right=of r1] {\bl{$r_2$}};
+\draw[->,line width=1mm] (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause
+\node (r3) [right=of r2] {\bl{$r_3$}};
+\draw[->,line width=1mm] (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause
+\node (r4) [right=of r3] {\bl{$r_4$}};
+\draw[->,line width=1mm] (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause
+\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$\;\;nullable?$}}};\pause
+\node (v4) [below=of r4] {\bl{$v_4$}};
+\draw[->,line width=1mm] (r4) -- (v4);\pause
+\node (v3) [left=of v4] {\bl{$v_3$}};
+\draw[->,line width=1mm] (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause
+\node (v2) [left=of v3] {\bl{$v_2$}};
+\draw[->,line width=1mm] (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause
+\node (v1) [left=of v2] {\bl{$v_1$}};
+\draw[->,line width=1mm] (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause
+\draw[->,line width=0.5mm] (r3) -- (v3);
+\draw[->,line width=0.5mm] (r2) -- (v2);
+\draw[->,line width=0.5mm] (r1) -- (v1);
+\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
+\end{tikzpicture}
+\end{center}
+
+\only<10>{
+The original ideas of Sulzmann and Lu are the \bl{\textit{mkeps}}
+and \bl{\textit{inj}} functions (ommitted here).}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t,squeeze]
+\frametitle{Sulzmann \& Lu Paper}
+
+\begin{itemize}
+\item I have no doubt the algorithm is correct ---
+ the problem is I do not believe their proof.
+
+ \begin{center}
+ \begin{bubble}[10cm]\small
+ ``How could I miss this? Well, I was rather careless when
+ stating this Lemma :)\smallskip
+
+ Great example how formal machine checked proofs (and
+ proof assistants) can help to spot flawed reasoning steps.''
+ \end{bubble}
+ \end{center}\pause
+
+ \begin{center}
+ \begin{bubble}[10cm]\small
+ ``Well, I don't think there's any flaw. The issue is how to
+ come up with a mechanical proof. In my world mathematical
+ proof $=$ mechanical proof doesn't necessarily hold.''
+ \end{bubble}
+ \end{center}\pause
+
+\end{itemize}
+
+ \only<3>{%
+ \begin{textblock}{11}(1,4.4)
+ \begin{center}
+ \begin{bubble}[10.9cm]\small\centering
+ \includegraphics[scale=0.37]{pics/msbug.png}
+ \end{bubble}
+ \end{center}
+ \end{textblock}}
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}The Proof Idea\\[-1mm] by Sulzmann \& Lu
+\end{tabular}}
+
+\begin{itemize}
+\item introduce an inductively defined ordering relation
+\bl{$v \succ_r v'$} which captures the idea of POSIX matching
+
+\item the algorithm returns the maximum of all possible
+ values that are possible for a regular expression.\pause
+ \bigskip\small
+
+\item the idea is from a paper by Cardelli \& Frisch about
+GREEDY matching (GREEDY $=$ preferring instant gratification to delayed
+repletion):
+
+\item e.g.~given \bl{$(a + (b + ab))^*$} and string \bl{$ab$}
+
+\begin{center}
+\begin{tabular}{ll}
+GREEDY: & \bl{$[Left(a), Right(Left(b)]$}\\
+POSIX: & \bl{$[Right(Right(Seq(a, b))))]$}
+\end{tabular}
+\end{center}
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{}
+\centering
+
+
+\bl{\infer{\vdash Empty : \epsilon}{}}\hspace{15mm}
+\bl{\infer{\vdash Char(c): c}{}}\bigskip
+
+\bl{\infer{\vdash Seq(v_1, v_2) : r_1\cdot r_2}{\vdash v_1 : r_1 \quad \vdash v_2 : r_2}}
+\bigskip
+
+\bl{\infer{\vdash Left(v) : r_1 + r_2}{\vdash v : r_1}}\hspace{15mm}
+\bl{\infer{\vdash Right(v): r_1 + r_2}{\vdash v : r_2}}\bigskip
+
+\bl{\infer{\vdash [] : r^*}{}}\hspace{15mm}
+\bl{\infer{\vdash [v_1,\ldots, v_n] : r^*}
+ {\vdash v_1 : r \quad\ldots\quad \vdash v_n : r}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}<1>[c]
+\frametitle{}
+\small
+
+%\begin{tabular}{@{}lll@{}}
+%\bl{$POSIX(v, r)$} & \bl{$\dn$} & \bl{$\vdash v : r$}\\
+% & & \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v|
+% \Rightarrow v \succ_{\alert<2>{r}} v')$}
+%\end{tabular}\bigskip\bigskip\bigskip
+
+
+\centering
+
+%\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}
+% {v_1 = v'_1 \quad v_2 \succ_{\alert<2>{r_2}} v'_2}}\hspace{3mm}
+%\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}
+% {v_1 \not= v'_1 \quad v_1 \succ_{\alert<2>{r_1}} v'_1}}
+%\bigskip
+
+%\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
+% {v \succ_{\alert<2>{r_1}} v'}}\hspace{15mm}
+%\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
+% {v \succ_{\alert<2>{r_2}} v'}}\bigskip\medskip
+
+%\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
+% {length |v| \ge length |v'|}}\hspace{15mm}
+%\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
+% {length |v| > length |v'|}}\bigskip
+
+%\bl{$\big\ldots$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Problems}
+
+\begin{itemize}
+\item Sulzmann: \ldots Let's assume \bl{$v$} is not
+ a $POSIX$ value, then there must be another one
+ \ldots contradiction.\bigskip\pause
+
+\item Exists?
+
+\begin{center}
+\bl{$L(r) \not= \varnothing \;\Rightarrow\; \exists v.\;POSIX(v, r)$}
+\end{center}\bigskip\bigskip\pause
+
+\item in the sequence case
+\bl{$Seq(v_1, v_2)\succ_{r_1\cdot r_2} Seq(v_1', v_2')$},
+the induction hypotheses require
+\bl{$|v_1| = |v'_1|$} and \bl{$|v_2| = |v'_2|$},
+but you only know
+
+\begin{center}
+\bl{$|v_1| \;@\; |v_2| = |v'_1| \;@\; |v'_2|$}
+\end{center}\pause\small
+
+\item although one begins with the assumption that the two
+values have the same flattening, this cannot be maintained
+as one descends into the induction (alternative, sequence)
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Our Solution}
+
+\begin{itemize}
+\item a direct definition of what a POSIX value is, using
+the relation \bl{$s \in r \to v$} (specification):\medskip
+
+\begin{center}
+\bl{\infer{[] \in \epsilon \to Empty}{}}\hspace{15mm}
+\bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip
+
+\bl{\infer{s \in r_1 + r_2 \to Left(v)}
+ {s \in r_1 \to v}}\hspace{10mm}
+\bl{\infer{s \in r_1 + r_2 \to Right(v)}
+ {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip
+
+\bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}
+ {\small\begin{array}{l}
+ s_1 \in r_1 \to v_1 \\
+ s_2 \in r_2 \to v_2 \\
+ \neg(\exists s_3\,s_4.\; s_3 \not= []
+ \wedge s_3 @ s_4 = s_2 \wedge
+ s_1 @ s_3 \in L(r_1) \wedge
+ s_4 \in L(r_2))
+ \end{array}}}
+
+\bl{\ldots}
+\end{center}
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Properties}
+
+It is almost trival to prove:
+
+\begin{itemize}
+\item Uniqueness
+\begin{center}
+If \bl{$s \in r \to v_1$} and \bl{$s \in r \to v_2$} then
+\bl{$v_1 = v_2$}.
+\end{center}\bigskip
+
+\item Correctness
+\begin{center}
+\bl{$lexer(r, s) = v$} if and only if \bl{$s \in r \to v$}
+\end{center}
+\end{itemize}\bigskip\bigskip\pause
+
+
+You can now start to implement optimisations and derive
+correctness proofs for them. But we still do not know whether
+
+\begin{center}
+\bl{$s \in r \to v$}
+\end{center}
+
+is a POSIX value according to Sulzmann \& Lu's definition
+(biggest value for \bl{$s$} and \bl{$r$})
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Conclusion}
+
+\begin{itemize}
+
+\item we replaced the POSIX definition of Sulzmann \& Lu by a
+ new definition (ours is inspired by work of Vansummeren,
+ 2006)\medskip
+
+\item their proof contained small gaps (acknowledged) but had
+ also fundamental flaws\medskip
+
+\item now, its a nice exercise for theorem proving\medskip
+
+\item some optimisations need to be applied to the algorithm
+ in order to become fast enough\medskip
+
+\item can be used for lexing, is a small beautiful functional
+ program
+
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[b]
+ \frametitle{
+ \begin{tabular}{c}
+ \mbox{}\\[13mm]
+ \alert{\LARGE Questions?}
+ \end{tabular}}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+