
diff -r 1a92233763bd -r cf8ebf62bded 9ms/ecoop_paper.tex
--- a/9ms/ecoop_paper.tex	Sat Jun 29 12:28:49 2019 +0100
+++ b/9ms/ecoop_paper.tex	Sun Jun 30 19:47:18 2019 +0100
@@ -1,6 +1,7 @@
 \documentclass[a4paper,UKenglish]{lipics}
 \usepackage{graphic}
 \usepackage{data}
+\usepackage{tikz-cd}
 % \documentclass{article}
 %\usepackage[utf8]{inputenc}
 %\usepackage[english]{babel}
@@ -228,9 +229,117 @@
 
 \section{The Algorithms by  Brzozowski, and Sulzmann and Lu}
 
-Suppose regular expressions are given by the following grammar (for
-the moment ignore the grammar for values on the right-hand side):
+Suppose regular expressions are given by the following grammar:
+
+
+\begin{center}
+
+		\begin{tabular}{@{}rrl@{}}
+			\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
+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}
+
+ %Assuming the classic notion of a
+%\emph{language} of a regular expression, written $L(\_)$, t
+The main
+property of the derivative operation is that
+
+\begin{center}
+$c\!::\!s \in L(r)$ holds
+if and only if $s \in L(r\backslash c)$.
+\end{center}
+
+\noindent
+So if we want to find out whether a string $s$
+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:
+\begin{center}
+\begin{tabular}{lcl}
+$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
+$r \backslash \epsilon $ & $\dn$ & $r$
+\end{tabular}
+\end{center}
+
+
+We obtain a simple and elegant regular
+expression matching algorithm: 
+\begin{definition}{matcher}
+\[
+match\;s\;r \;\dn\; nullable(r\backslash s)
+\]
+\end{definition}
+
+ 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
+generalised to cover extended regular expression constructors such as
+the not-regular expression, written $\neg\,r$, or bounded repetitions
+(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
+straightforwardly realised within the classic automata approach.
+
+
+One limitation, however, of Brzozowski's algorithm is that it only
+produces a YES/NO answer for whether a string is being matched by a
+regular expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this
+algorithm to allow generation of an actual matching, called a
+\emph{value}.  
 
 \begin{center}
 	\begin{tabular}{c@{\hspace{20mm}}c}
@@ -259,71 +368,10 @@
 \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
-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
-In this definition $\nullable(\_)$ stands for a simple recursive
-function that tests whether a regular expression can match the empty
-string (its definition is omitted). Assuming the classic notion of a
-\emph{language} of a regular expression, written $L(\_)$, the main
-property of the derivative operation is that
+ Here we put the regular expression and values of the same shape on the same level to illustrate the corresponding relation between them. \\
+ 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$.\\
 
-\begin{center}
-$c\!::\!s \in L(r)$ holds
-if and only if $s \in L(r\backslash c)$.
-\end{center}
-
-\noindent
-The beauty of derivatives is that they lead to a really simple regular
-expression matching algorithm: To find out whether a string $s$
-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. 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
-generalised to cover extended regular expression constructors such as
-the not-regular expression, written $\neg\,r$, or bounded repetitions
-(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
-straightforwardly realised within the classic automata approach.
-
-
-One limitation, however, of Brzozowski's algorithm is that it only
-produces a YES/NO answer for whether a string is being matched by a
-regular expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this
-algorithm to allow generation of an actual matching, called a
-\emph{value}---see the grammar above for its definition.  Assuming a
-regular expression matches a string, values encode the information of
-\emph{how} the string is matched by the regular expression---that is,
-which part of the string is matched by which part of the regular
-expression. To illustrate this consider the string $xy$ and the
+ 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
@@ -353,10 +401,17 @@
 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. As mentioned before, from this
-value we can extract the information \emph{how} a regular expression
-matched a string. We omit the details here on how Sulzmann and Lu
-achieved this~(see \cite{Sulzmann2014}). Rather, we shall focus next on the
+corresponding POSIX value is computed. The whole process looks like this diagram:\\
+\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] \\
+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}
+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:
+
+ After this, we inject back the characters one by one, in reverse order as they were chopped off, to build the parse tree $v_i$ for how the regex $r_i$ matches the string $s_i$($s_i$ means the string s with the first $i$ characters being chopped off) from the previous parse tree. After $n$ transformations, we get the parse tree for how $r_0$ matches $s$, exactly as we wanted.
+An inductive proof can be routinely established.
+We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}. Rather, we shall focus next on the
 process of simplification of regular expressions, which is needed in
 order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann
 and Lu's algorithms.  This is where the PhD-project hopes to advance
@@ -412,12 +467,8 @@
 where $bs$ stands for bitsequences, and $as$ (in \textit{ALTS}) for a
 list of annotated regular expressions. These bitsequences encode
 information about the (POSIX) value that should be generated by the
-Sulzmann and Lu algorithm. There are operations that can transform the
-usual (un-annotated) regular expressions into annotated regular
-expressions, and there are operations for encoding/decoding values to
-or from bitsequences. For example the encoding function for values is
-defined as follows:
-
+Sulzmann and Lu algorithm. Bitcodes are essentially incomplete values.
+This can be straightforwardly seen in the following transformation: 
 \begin{center}
 \begin{tabular}{lcl}
   $\textit{code}(\Empty)$ & $\dn$ & $[]$\\
@@ -430,18 +481,32 @@
                                                  code(\Stars\,vs)$
 \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
+\\
 
-\noindent
-where $\Z$ and $\S$ are arbitrary names for the ``bits'' in the
-bitsequences. Although this encoding is ``lossy'' in the sense of not
-recording all details of a value, Sulzmann and Lu have defined the
-decoding function such that with additional information (namely the
-corresponding regular expression) a value can be precisely extracted
-from a bitsequence.
+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
+\\
+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
+\\
+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
+\\
+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
 is that we can apply rather aggressive (in terms of size)
-simplification rules in order to keep derivatives small.  We have
+simplification rules in order to keep derivatives small.  
+
+We have
 developed such ``aggressive'' simplification rules and generated test
 data that show that the expected bound can be achieved. Obviously we
 could only partially cover  the search space as there are infinitely
@@ -455,7 +520,7 @@
 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
-subsequent copies can be prunned from the regular expression.
+subsequent copies can be pruned from the regular expression.
 
 We are currently engaged with proving that our simplification rules
 actually do not affect the POSIX value that should be generated by the




