cst_tests: comparison ninems/ninems.tex

equal deleted inserted replaced

-:f70e9ab4e680
+:97c9ac95194d
 regular expressions \cite{Brzozowski1964}. We shall briefly explain
 the algorithms next.
 \section{The Algorithms by  Brzozowski, and Sulzmann and Lu}
-Suppose regular expressions are given by the following grammar:
+Suppose regular expressions are given by the following grammar:\\
+			$r$  $::=$   $\ZERO$ $\mid$  $\ONE$
+			 $\mid$  $c$
-\begin{center}
+			 $\mid$  $r_1 \cdot r_2$
-%TODO
+			 $\mid$  $r_1 + r_2$
-		\begin{tabular}{@{}rrl@{}}
+			 $\mid$  $r^*$
-			\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
-			$r$ & $::=$  & $\ZERO$\\
-			& $\mid$ & $\ONE$   \\
-			& $\mid$ & $c$          \\
-			& $\mid$ & $r_1 \cdot r_2$\\
-			& $\mid$ & $r_1 + r_2$   \\
-			& $\mid$ & $r^*$
-		\end{tabular}
-\end{center}
 \noindent
 The intended meaning of the regular expressions is as usual: $\ZERO$
 cannot match any string, $\ONE$ can match the empty string, the
 character regular expression $c$ can match the character $c$, and so
 on. The brilliant contribution by Brzozowski is the notion of
 \emph{derivatives} of regular expressions.  The idea behind this
 notion is as follows: suppose a regular expression $r$ can match a
 string of the form $c\!::\! s$ (that is a list of characters starting
 with $c$), what does the regular expression look like that can match
-just $s$? Brzozowski gave a neat answer to this question. He defined
+just $s$? Brzozowski gave a neat answer to this question. He started with the definition of $nullable$:
-the following operation on regular expressions, written
-$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
-\begin{center}
-\begin{tabular}{lcl}
-		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\
-		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\
-		$d \backslash c$     & $\dn$ &
-		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
-$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
-$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, \epsilon \in L(r_1)$\\
-	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
-	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
-	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\
-\end{tabular}
-\end{center}
-\noindent
-The $\mathit{if}$ condition in the definition of $(r_1 \cdot r_2) \backslash c$ involves a membership testing: $\epsilon \overset{?}{\in} L(r_1)$.
-Such testing is easily implemented by the following simple recursive function $\nullable(\_)$:
 \begin{center}
 		\begin{tabular}{lcl}
 			$\nullable(\ZERO)$     & $\dn$ & $\mathit{false}$ \\
 			$\nullable(\ONE)$      & $\dn$ & $\mathit{true}$ \\
 			$\nullable(c)$ 	       & $\dn$ & $\mathit{false}$ \\
 			$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
 			$\nullable(r_1\cdot r_2)$  & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
 			$\nullable(r^*)$       & $\dn$ & $\mathit{true}$ \\
 		\end{tabular}
 	\end{center}
+The function tests whether the empty string is in $L(r)$.
+He then defined
+the following operation on regular expressions, written
+$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
+\begin{center}
+\begin{tabular}{lcl}
+		$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\
+		$\ONE \backslash c$  & $\dn$ & $\ZERO$\\
+		$d \backslash c$     & $\dn$ &
+		$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
+$(r_1 + r_2)\backslash c$     & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
+$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
+	&   & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
+	&   & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
+	$(r^*)\backslash c$           & $\dn$ & $(r\backslash c) \cdot r^*$\\
+\end{tabular}
+\end{center}
+\noindent
 %Assuming the classic notion of a
 %\emph{language} of a regular expression, written $L(\_)$, t
 The main
 property of the derivative operation is that
 matches with a regular expression $r$, build the derivatives of $r$
 w.r.t.\ (in succession) all the characters of the string $s$. Finally,
 test whether the resulting regular expression can match the empty
 string.  If yes, then $r$ matches $s$, and no in the negative
 case.\\
-If we define the successive derivative operation to be like this:
+We can generalise the derivative operation for strings like this:
 \begin{center}
 \begin{tabular}{lcl}
 $r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
 $r \backslash \epsilon $ & $\dn$ & $r$
 \end{tabular}
 \end{center}
 For us the main advantage is that derivatives can be
 straightforwardly implemented in any functional programming language,
 and are easily definable and reasoned about in theorem provers---the
 definitions just consist of inductive datatypes and simple recursive
 functions. Moreover, the notion of derivatives can be easily
 	\end{tabular}
 \end{center}
 \noindent
 Here we put the regular expression and values of the same shape on the same level to illustrate the corresponding relation between them.
+The flatten notation $| v |$ means extracting the characters in the value $v$ to form a string. For example, $|\mathit{Seq} \, \mathit{Char(c)} \, \mathit{Char(d)}|$ = $cd$. We omit this straightforward definition.
-Values are a way of expressing parse trees(the tree structure that tells how a sub-regex matches a substring). For example, $\Seq\,v_1\, v_2$ tells us how the string $|v_1| \cdot |v_2|$ matches the regex $r_1 \cdot r_2$: $r_1$ matches $|v_1|$ and $r_2$ matches $|v_2|$. Exactly how these two are matched are contained in the sub-structure of $v_1$ and $v_2$. The flatten notation $| v |$ means extracting the characters in the value $v$ to form a string. For example, $|\mathit{Seq} \, \mathit{Char(c)} \, \mathit{Char(d)}|$ = $cd$.
+Values are a way of expressing parse trees(the tree structure that tells how a sub-regex matches a substring). For example, $\Seq\,v_1\, v_2$ tells us how the string $|v_1| \cdot |v_2|$ matches the regex $r_1 \cdot r_2$: $r_1$ matches $|v_1|$ and $r_2$ matches $|v_2|$. Exactly how these two are matched are contained in the sub-structure of $v_1$ and $v_2$.
 To give a concrete example of how value works, consider the string $xy$ and the
 regular expression $(x + (y + xy))^*$. We can view this regular
 expression as a tree and if the string $xy$ is matched by two Star
 ``iterations'', then the $x$ is matched by the left-most alternative
 The contribution of Sulzmann and Lu is an extension of Brzozowski's
 algorithm by a second phase (the first phase being building successive
 derivatives). In this second phase, for every successful match the
 corresponding POSIX value is computed. The whole process looks like the following diagram(the working flow of the simple matching algorithm that just gives a $YES/NO$ answer is provided on the right for the purpose of comparison):\\
 \begin{tikzcd}
-r_0 \arrow[r, "c_0"]  \arrow[d] & r_1 \arrow[r, "c_1"] \arrow[d] & r_2 \arrow[r, dashed] \arrow[d] & r_n \arrow[d, "mkeps" description] \\
+r_0 \arrow[r, "\backslash c_0"]  \arrow[d] & r_1 \arrow[r, "\backslash c_1"] \arrow[d] & r_2 \arrow[r, dashed] \arrow[d] & r_n \arrow[d, "mkeps" description] \\
 v_0           & v_1 \arrow[l,"inj_{r_0} c_0"]                & v_2 \arrow[l, "inj_{r_1} c_1"]              & v_n \arrow[l, dashed]
+\end{tikzcd}
+\begin{tikzcd}
+r_0 \arrow[r, "\backslash c_0"]  & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed]  & r_n
 \end{tikzcd}
 We shall briefly explain this interesting process.\\ For the convenience of explanation, we have the following notations: the regular expression $r$ used for matching is also called $r_0$ and the string $s$ is composed of $n$ characters $c_0 c_1 ... c_{n-1}$.
 First, we do the derivative operation on $r_0$, $r_1$, ..., using characters $c_0$, $c_1$, ...  until we get the final derivative $r_n$.We test whether it is $nullable$ or not. If no we know immediately the string does not match the regex. If yes, we start building the parse tree incrementally. We first call $mkeps$(which stands for make epsilon--make the parse tree for the empty word epsilon) to construct the parse tree $v_n$ for how the final derivative $r_n$ matches the empty string:
 \end{tabular}
 \end{center}
 where $\Z$ and $\S$ are arbitrary names for the bits in the
 bitsequences.
 Here code encodes a value into a bitsequence by converting Left into $\Z$, Right into $\S$, the start point of a non-empty star iteration into $\S$, and the border where a local star terminates into $\Z$. This conversion is apparently lossy, as it throws away the character information, and does not decode the boundary between the two operands of the sequence constructor. Moreover, with only the bitcode we cannot even tell whether the $\S$s and $\Z$s are for $Left/Right$ or $Stars$. The reason for choosing this compact way of storing information is that the relatively small size of bits can be easily moved around during the lexing process. In order to recover the bitcode back into values, we will need the regular expression as the extra information and decode them back into value:\\
-TODO: definition of decode
+\begin{definition}[Bitdecoding of Values]\mbox{}
-\\
+\begin{center}
+\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
+$\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
+$\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
+$\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
+$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
+(\Left\,v, bs_1)$\\
+$\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
+$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
+(\Right\,v, bs_1)$\\
+$\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
+$\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
+& &   $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
+& &   \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
+$\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
+$\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ &
+$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
+& &   $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
+& &   \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
+$\textit{decode}\,bs\,r$ & $\dn$ &
+$\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
+& & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
+\textit{else}\;\textit{None}$
+\end{tabular}
+\end{center}
+\end{definition}
 To do lexing using annotated regular expressions, we shall first transform the
 usual (un-annotated) regular expressions into annotated regular
 expressions:\\
-TODO: definition of internalise
+\begin{definition}
-\\
+\begin{center}
+\begin{tabular}{lcl}
+$(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\
+$(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
+$(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\
+$(r_1 + r_2)^\uparrow$ & $\dn$ &
+$\textit{ALT}\;[]\,(\textit{fuse}\,[\Z]\,r_1^\uparrow)\,
+(\textit{fuse}\,[\S]\,r_2^\uparrow)$\\
+$(r_1\cdot r_2)^\uparrow$ & $\dn$ &
+$\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\
+$(r^*)^\uparrow$ & $\dn$ &
+$\textit{STAR}\;[]\,r^\uparrow$\\
+\end{tabular}
+\end{center}
+\end{definition}
 Then we do successive derivative operations on the annotated regular expression. This derivative operation is the same as what we previously have for the simple regular expressions, except that we take special care of the bits to store the parse tree information:\\
-TODO: bder
+\begin{definition}{bder}
-\\
+\begin{center}
+\begin{tabular}{@{}lcl@{}}
+$(\textit{ZERO})\backslash c$ & $\dn$ & $\textit{ZERO}$\\
+$(\textit{ONE}\;bs)\backslash c$ & $\dn$ & $\textit{ZERO}$\\
+$(\textit{CHAR}\;bs\,d)\backslash c$ & $\dn$ &
+$\textit{if}\;c=d\; \;\textit{then}\;
+\textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\
+$(\textit{ALT}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
+$\textit{ALT}\,bs\,(a_1\backslash c)\,(a_2\backslash c)$\\
+$(\textit{SEQ}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
+$\textit{if}\;\textit{bnullable}\,a_1$\\
+& &$\textit{then}\;\textit{ALT}\,bs\,(\textit{SEQ}\,[]\,(a_1\backslash c)\,a_2)$\\
+& &$\phantom{\textit{then}\;\textit{ALT}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\backslash c))$\\
+& &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\backslash c)\,a_2$\\
+$(\textit{STAR}\,bs\,a)\backslash c$ & $\dn$ &
+$\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\backslash c))\,
+(\textit{STAR}\,[]\,r)$
+\end{tabular}
+\end{center}
+\end{definition}
 This way, we do not have to use an injection function and a second phase, but instead only need to collect the bits while running $mkeps$:
-TODO: mkepsBC
+\begin{definition}[\textit{bmkeps}]\mbox{}
-\\
+\begin{center}
+\begin{tabular}{lcl}
+$\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\
+$\textit{bmkeps}\,(\textit{ALT}\,bs\,a_1\,a_2)$ & $\dn$ &
+$\textit{if}\;\textit{bnullable}\,a_1$\\
+& &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a_1$\\
+& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,a_2$\\
+$\textit{bmkeps}\,(\textit{SEQ}\,bs\,a_1\,a_2)$ & $\dn$ &
+$bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
+$\textit{bmkeps}\,(\textit{STAR}\,bs\,a)$ & $\dn$ &
+$bs \,@\, [\S]$
+\end{tabular}
+\end{center}
+\end{definition}
 and then decode the bits using the regular expression. The whole process looks like this:\\
 r
 \\
 The main point of the bitsequences and annotated regular expressions
 	\EndCase
 \EndSwitch
 \EndProcedure
 \end{algorithmic}
 \end{algorithm}
+With this simplification our previous $(a + aa)^*$ example's 8000 nodes will be reduced to only 6.
 Another modification is that we use simplification rules
 inspired by Antimirov's work on partial derivatives. They maintain the
 idea that only the first ``copy'' of a regular expression in an
 alternative contributes to the calculation of a POSIX value. All

changeset 36	97c9ac95194d
parent 35	f70e9ab4e680
child 37	17d8e7599a01