24 \title{\bf POSIX Lexing with\\ 

    24 \newcommand\grid[1]{%

    25        \bf Derivatives of Regular Expressions\\

    25 	\begin{tikzpicture}[baseline=(char.base)]

    26        \bf (Proof Pearl)}

    26 	\path[use as bounding box]

    27 	(0,0) rectangle (1em,1em);

    28 	\draw[red!50, fill=red!20]

    29 	(0,0) rectangle (1em,1em);

    30 	\node[inner sep=1pt,anchor=base west]

    31 	(char) at (0em,\gridraiseamount) {#1};

    32 	\end{tikzpicture}}

    33 \newcommand\gridraiseamount{0.12em}

    34 

    35 \makeatletter

    36 \newcommand\Grid[1]{%

    37 	\@tfor\z:=#1\do{\grid{\z}}}

    38 \makeatother	

    39 

    40 \newcommand\Vspace[1][.3em]{%

    41 	\mbox{\kern.06em\vrule height.3ex}%

    42 	\vbox{\hrule width#1}%

    43 	\hbox{\vrule height.3ex}}

    44 

    45 \def\VS{\Vspace[0.6em]}

    46 

    47 

    48 \title[POSIX Lexing with Derivatives of Regexes]

    49 {\bf POSIX Lexing with\\ 

    50 	\bf Derivatives of Regular Expressions\\

    51 	\bf (Proof Pearl)}

   187 	For example: \smath{r_{keywords} + r_{identifiers}} (fix graphics below)

   213 	For example: \smath{r_{keywords} + r_{identifiers}}

   188 

   214 

   189 		\begin{center}

   215 		\begin{itemize}

   190 		\texttt{iffoo\_bla} 

   216 			\item \smath{\texttt{\Grid{iffoo\VS bla}}} 

   191 		\end{center}

   217 			

   192 		

   218 			\item \smath{\texttt{\Grid{if\VS bla}}}

   193 		\begin{center}

   219 		\end{itemize}	

   194 		\texttt{if\_bla} 

   195 		\end{center}	

   215 	matching, which indicates that most POSIX mathcers are buggy.

   239 	matching, which indicates that most POSIX matchcers are buggy.

   235 	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   259 	

   236 	

   237 	\begin{frame}

   238 	\frametitle{Regular Expressions and Values}

   239 	Regular expressions and their corresponding values (for how a 

   240 	regular expression matched string): 

   241     \begin{columns}[c] % the "c" option specifies center vertical alignment

   242     \column{.5\textwidth} % column designated by a command

   243      	\begin{tabular}{ l l l }

   244 			$r$ & ::= 		& $\varnothing$ 	\\

   245 			    & $\mid$	& $\epsilon$ 		\\

   246 			    & $\mid$	& $c$ 				\\

   247 			    & $\mid$	& $r_1 \cdot r_2$	\\

   248 			    & $\mid$	& $r_1 + r_2$		\\

   249 			    & $\mid$	& $r^*$				\\

   250 		\end{tabular}

   251     \column{.5\textwidth}

   252      	\begin{tabular}{ l l l }

   253 			$v$ & ::= 		& $\varnothing$ 	\\

   254 			    & $\mid$	& $Empty$ 			\\

   255 			    & $\mid$	& $Char$($c$) 		\\

   256 			    & $\mid$	& $Seq$($v_1.v_2$)	\\

   257 			    & $\mid$	& $Left$($v$)		\\

   258 			    & $\mid$	& $Right$($v$)		\\

   259 			    & $\mid$	& []				\\

   260 			    & $\mid$	& [$v_1,...,v_n$]

   261 		\end{tabular}

   262     \end{columns}

   263     There is also a notion of a string behind a value $\mid v \mid$

   264 	\end{frame}

   274 	\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]

   269 		\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]

   277 		\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {$der\,a$};\pause

   272 		\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {$der\,a$};

   279 		\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {$der\,b$};\pause

   274 		\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {$der\,b$};

   281 		\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {$der\,c$};\pause

   276 		\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {$der\,c$};

   292 		\draw[->,line width=0.5mm]  (r3) -- (v3);

   287 		%\draw[->,line width=0.5mm]  (r3) -- (v3);

   293 		\draw[->,line width=0.5mm]  (r2) -- (v2);

   288 		%\draw[->,line width=0.5mm]  (r2) -- (v2);

   294 		\draw[->,line width=0.5mm]  (r1) -- (v1);

   289 		%\draw[->,line width=0.5mm]  (r1) -- (v1);

   295 	\end{tikzpicture}

   290 		\onslide<1->

   291 		\end{tikzpicture}

   303 	\frametitle{Nullable, Mkeps and Injection Functions}

   299 		\frametitle{Regular Expressions and Values}

   304 	

   300 		Regular expressions and their corresponding values (for how a 

   305 	\textbf{Nullable Function}

   301 		regular expression matched string):

   306 	\begin{tabular}{ l l l }

   302 		\vspace{5 mm} 

   307 		\textit{nullable} (\textbf{0}) & $\dn$ & \textit{False}\\

   303 		\begin{columns}[c] % the "c" option specifies center vertical alignment

   308 		\textit{nullable} (\textbf{1}) & $\dn$ & \textit{True}\\

   304 			\column{.4\textwidth} % column designated by a command

   309 		\textit{nullable} (c) & $\dn$ & \textit{False}\\

   305 			\begin{tabular}{ l l l }

   310 		\textit{nullable} ($r_1 + r_2$) & $\dn$ & \textit{nullable} $r_1$ $\lor$ \textit{nullable} $r_2$\\

   306 				\smath{r} & ::= 		& \smath{\Zero} 	\\

   311 		\textit{nullable} ($r_1 \cdot r_2$) & $\dn$ & \textit{nullable} $r_1$ $\land$ \textit{nullable} $r_2$\\

   307 				& $\mid$	& \smath{\One} 		\\

   312 		\textit{nullable} ($r^*$) & $\dn$ & \textit{True}\\

   308 				& $\mid$	& \smath{c} 				\\

   313 	\end{tabular}\\	

   309 				& $\mid$	& \smath{r_1 \cdot r_2}	\\

   314 	\vspace{3 mm}	

   310 				& $\mid$	& \smath{r_1 + r_2}		\\ \\

   311 				& $\mid$	& \smath{r^*}				\\

   312 			\end{tabular}

   313 			\column{.4\textwidth}

   314 			\begin{tabular}{ l l l }

   315 				

   316 				\smath{v} & ::= 		& \\

   317 				& $\mid$	& \smath{Empty} 			\\

   318 				& $\mid$	& \smath{Char(c)} 		\\

   319 				& $\mid$	& \smath{Seq(v_1\cdot v_2)}	\\

   320 				& $\mid$	& \smath{Left(v)}		\\

   321 				& $\mid$	& \smath{Right(v)}		\\

   322 				& $\mid$	& \smath{[v_1,...,v_n]}

   323 			\end{tabular}

   324 		\end{columns}

   325 		\vspace{5 mm}

   326 		There is also a notion of a string behind a value $\mid v \mid$

   327 	\end{frame}

   328 	

   329 	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   330 	

   331 	\begin{frame}

   332 	\frametitle{Mkeps and Injection Functions}

   333 		

   317 		\textit{mkeps} (\textbf{1}) 		& $\dn$ & () 	\\

   336 		\textit{mkeps} (\textbf{1}) 		& $\dn$ & \textit{Empty} 	\\

   329 	\frametitle{Nullable, Mkeps and Injection Functions}

   348 	\frametitle{Mkeps and Injection Functions}

   358 	to delayed repletion):

   377 	to delayed repletion)

   359 	

   378 	

   360 	\item e.g. given $(a + (b + ab))^{*}$ and string $ab$\\

   379 	%\item e.g. given $(a + (b + ab))^{*}$ and string $ab$\\

   361 	\begin{center}	

   380 	%\begin{center}	

   362 	\begin{tabular}{ll}

   381 	%\begin{tabular}{ll}

   363 	GREEDY: & $[Left(a), Right(Left(b))]$\\

   382 	%GREEDY: & $[Left(a), Right(Left(b))]$\\

   364 	POSIX: 	& $[Right(Right(Seq(a, b)))]$

   383 	%POSIX: 	& $[Right(Right(Seq(a, b)))]$

   365 	\end{tabular}

   384 	%\end{tabular}

   366 	\end{center}

   385 	%\end{center}

   373 	\begin{frame}

   392 %	\begin{frame}

   374 	\frametitle{POSIX Ordering Relation by Sulzmann \& Lu}

   393 %	\frametitle{POSIX Ordering Relation by Sulzmann \& Lu}

   375 	

   394 %	

   376 	\begin{center}

   395 %	\begin{center}

   377 		$\infer{\vdash Empty : \epsilon}{}$\hspace{15mm}	

   396 %		$\infer{\vdash Empty : \epsilon}{}$\hspace{15mm}	

   378 		$\infer{\vdash Char(c): c}{}$\bigskip

   397 %		$\infer{\vdash Char(c): c}{}$\bigskip

   379 		

   398 %		

   380 		$\infer{\vdash Seq(v_1, v_2) : r_1\cdot r_2}{\vdash v_1 : r_1 \quad \vdash v_2 : r_2}$

   399 %		$\infer{\vdash Seq(v_1, v_2) : r_1\cdot r_2}{\vdash v_1 : r_1 \quad \vdash v_2 : r_2}$

   381 		\bigskip

   400 %		\bigskip

   382 		

   401 %		

   383 		$\infer{\vdash Left(v) : r_1 + r_2}{\vdash v : r_1}$\hspace{15mm}

   402 %		$\infer{\vdash Left(v) : r_1 + r_2}{\vdash v : r_1}$\hspace{15mm}

   384 		$\infer{\vdash Right(v): r_1 + r_2}{\vdash v : r_2}$\bigskip

   403 %		$\infer{\vdash Right(v): r_1 + r_2}{\vdash v : r_2}$\bigskip

   385 		

   404 %		

   386 		$\infer{\vdash [] : r^*}{}$\hspace{15mm}

   405 %		$\infer{\vdash [] : r^*}{}$\hspace{15mm}

   387 		$\infer{\vdash [v_1,\ldots, v_n] : r^*}

   406 %		$\infer{\vdash [v_1,\ldots, v_n] : r^*}

   388 		{\vdash v_1 : r \quad\ldots\quad \vdash v_n : r}$

   407 %		{\vdash v_1 : r \quad\ldots\quad \vdash v_n : r}$

   389 	\end{center}

   408 %	\end{center}

   390 	

   409 %	

   391 	\end{frame}

   410 %	\end{frame}

   425 	\begin{frame}

   444 %	\begin{frame}

   426 		\frametitle{Problems}

   445 %		\frametitle{Problems}

   427 		

   446 %		

   428 		\begin{itemize}

   447 %		\begin{itemize}

   429 			\item I have no doubt the algorithm is correct --- 

   448 %			\item I have no doubt the algorithm is correct --- 

   430 			the problem is I do not believe their proof.

   449 %			the problem is I do not believe their proof.

   450 %			

   451 %			\begin{center}

   452 %				\small

   453 %				``How could I miss this? Well, I was rather careless when 

   454 %				stating this Lemma :)\smallskip

   455 %				

   456 %				Great example how formal machine checked proofs (and 

   457 %				proof assistants) can help to spot flawed reasoning steps.''

   458 %				

   459 %			\end{center}

   460 %			

   461 %			\begin{center}

   462 %				\small

   463 %				``Well, I don't think there's any flaw. The issue is how to 

   464 %				come up with a mechanical proof. In my world mathematical 

   465 %				proof $=$ mechanical proof doesn't necessarily hold.''

   466 %				

   467 %			\end{center}

   468 %			

   469 %		\end{itemize}	

   470 %		

   471 %	\end{frame}

   472 	

   473 	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   474 	

   475 	\begin{frame}

   476 		\frametitle{Our Solution}

   477 		

   478 	\begin{itemize}

   479 		\item A direct definition of what a POSIX value is, using the 

   480 		relation \smath{s \in r \to v} (our specification)\bigskip

   432 			\begin{center}

   482 	\begin{center}

   433 				\small

   483 		\smath{\infer{[] \in \One \to Empty}{}}\hspace{15mm}

   434 				``How could I miss this? Well, I was rather careless when 

   484 		\smath{\infer{[c] \in c \to Char(c)}{}}\bigskip\medskip

   435 				stating this Lemma :)\smallskip

   485 		

   436 				

   486 		\smath{\infer{s \in r_1 + r_2 \to Left(v)}

   437 				Great example how formal machine checked proofs (and 

   487 			{s \in r_1 \to v}}\hspace{10mm}

   438 				proof assistants) can help to spot flawed reasoning steps.''

   488 		\smath{\infer{s \in r_1 + r_2 \to Right(v)}

   439 				

   489 			{s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip

   440 			\end{center}

   490 		

   491 		\smath{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}

   492 			{\small\begin{array}{l}

   493 					s_1 \in r_1 \to v_1 \\

   494 					s_2 \in r_2 \to v_2 \\

   495 					\neg(\exists s_3\,s_4.\; s_3 \not= []

   496 					\wedge s_3 @ s_4 = s_2 \wedge

   497 					s_1 @ s_3 \in L(r_1) \wedge

   498 					s_4 \in L(r_2))

   499 				\end{array}}}

   500 				

   501 				{\ldots}           

   502 			\end{center}	

   442 			\begin{center}

   504 		\end{itemize}

   443 				\small

   444 				``Well, I don't think there's any flaw. The issue is how to 

   445 				come up with a mechanical proof. In my world mathematical 

   446 				proof $=$ mechanical proof doesn't necessarily hold.''

   447 				

   448 			\end{center}

   449 			

   450 		\end{itemize}	

   451 		

   452 	\end{frame}

   453 	

   454 	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   455 	

   456 	\begin{frame}

   457 	\frametitle{Our Solution}

   458 

   459 	\begin{itemize}

   460 	\item A direct definition of what a POSIX value is, using the 

   461 	relation $s \in r \to v$ (specification)

   462 	

   463 	\begin{center}

   464 		$\infer{[] \in \epsilon \to Empty}{}$\hspace{15mm}

   465 		$\infer{c \in c \to Char(c)}{}$\bigskip\medskip

   466 		

   467 		$\infer{s \in r_1 + r_2 \to Left(v)}

   468 		{s \in r_1 \to v}$\hspace{10mm}

   469 		$\infer{s \in r_1 + r_2 \to Right(v)}

   470 		{s \in r_2 \to v & s \not\in L(r_1)}$\bigskip\medskip

   471 		

   472 		$\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}

   473 		{\small\begin{array}{l}

   474 			s_1 \in r_1 \to v_1 \\

   475 			s_2 \in r_2 \to v_2 \\

   476 			\neg(\exists s_3\,s_4.\; s_3 \not= []

   477 			\wedge s_3 @ s_4 = s_2 \wedge

   478 			s_1 @ s_3 \in L(r_1) \wedge

   479 			s_4 \in L(r_2))

   480 			\end{array}}$

   481 		\\

   482 		\bigskip

   483 		...

   484 	\end{center}	

   485 	

   486 	\end{itemize}

   510 	correctness proofs for them. But we still do not know whether

   528 	correctness proofs for them.% But we still do not know whether

   511 	

   529 %	

   512 	\begin{center}

   530 %	\begin{center}

   513 	$s \in r \to v$ 

   531 %	$s \in r \to v$ 

   514 	\end{center}

   532 %	\end{center}

   515 	

   533 %	

   516 	is a POSIX value according to Sulzmann \& Lu's definition

   534 %	is a POSIX value according to Sulzmann \& Lu's definition

   517 	(biggest value for $s$ and $r$)

   535 %	(biggest value for $s$ and $r$)

   518 	\end{frame}

   536 	\end{frame}

   519 	

   537 	

   520 	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   538 		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   521 	

   539 		

   522 	\begin{frame}

   540 		\begin{frame}

   523 		\frametitle{Conclusions}

   541 			\frametitle{Conclusions}

   524 		

   525 		\begin{itemize}

   527 			\item We replaced the POSIX definition of Sulzmann \& Lu by a

   543 			\begin{itemize}

   528 			new definition (ours is inspired by work of Vansummeren,

   544 				

   529 			2006)\medskip

   545 				\item Sulzmann and Lu's informal proof contained small gaps (acknowledged) but we believe it had

   530 			

   546 				also fundamental flaws\medskip

   531 			\item Their proof contained small gaps (acknowledged) but had

   547 				

   532 			also fundamental flaws\medskip

   548 				\item We replaced the POSIX definition of Sulzmann \& Lu by a

   533 			

   549 				new definition (ours is inspired by work of Vansummeren,

   534 			\item Now, its a nice exercise for theorem proving\medskip

   550 				2006)\medskip

   535 			

   551 				

   536 			\item Some optimisations need to be applied to the algorithm

   552 				\item Now, its a nice exercise for theorem proving\medskip

   537 			in order to become fast enough\medskip

   553 				

   538 			

   554 				\item Some optimisations need to be applied to the algorithm

   539 			\item Can be used for lexing, is a small beautiful functional

   555 				in order to become fast enough\medskip

   540 			program

   556 				

   541 			

   557 				\item Can be used for lexing, is a small beautiful functional

   542 		\end{itemize}

   558 				program

   543 	\end{frame}

   559 				

   544 	

   560 			\end{itemize}

   561 		\end{frame}

   562