diff -r dc0cdfc5fc66 -r fb7472a29058 etnms/20200205.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/etnms/20200205.tex Wed Feb 05 22:55:21 2020 +0000 @@ -0,0 +1,1836 @@ +\documentclass[a4paper,UKenglish]{lipics} +\usepackage{graphic} +\usepackage{data} +\usepackage{tikz-cd} +\usepackage{tikz} +\usetikzlibrary{graphs} +\usetikzlibrary{graphdrawing} +\usegdlibrary{trees} +%\usepackage{algorithm} +\usepackage{amsmath} +\usepackage{xcolor} +\usepackage[noend]{algpseudocode} +\usepackage{enumitem} +\usepackage{nccmath} +\usepackage{soul} + +\definecolor{darkblue}{rgb}{0,0,0.6} +\hypersetup{colorlinks=true,allcolors=darkblue} +\newcommand{\comment}[1]% +{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}} + +% \documentclass{article} +%\usepackage[utf8]{inputenc} +%\usepackage[english]{babel} +%\usepackage{listings} +% \usepackage{amsthm} +%\usepackage{hyperref} +% \usepackage[margin=0.5in]{geometry} +%\usepackage{pmboxdraw} + +\title{POSIX Regular Expression Matching and Lexing} +\author{Chengsong Tan} +\affil{King's College London\\ +London, UK\\ +\texttt{chengsong.tan@kcl.ac.uk}} +\authorrunning{Chengsong Tan} +\Copyright{Chengsong Tan} + +\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% +\newcommand{\ZERO}{\mbox{\bf 0}} +\newcommand{\ONE}{\mbox{\bf 1}} +\def\erase{\textit{erase}} +\def\bders{\textit{bders}} +\def\lexer{\mathit{lexer}} +\def\blexer{\textit{blexer}} +\def\fuse{\textit{fuse}} +\def\flatten{\textit{flatten}} +\def\map{\textit{map}} +\def\blexers{\mathit{blexer\_simp}} +\def\simp{\mathit{simp}} +\def\mkeps{\mathit{mkeps}} +\def\bmkeps{\textit{bmkeps}} +\def\inj{\mathit{inj}} +\def\Empty{\mathit{Empty}} +\def\Left{\mathit{Left}} +\def\Right{\mathit{Right}} +\def\Stars{\mathit{Stars}} +\def\Char{\mathit{Char}} +\def\Seq{\mathit{Seq}} +\def\Der{\mathit{Der}} +\def\nullable{\mathit{nullable}} +\def\Z{\mathit{Z}} +\def\S{\mathit{S}} +\def\flex{\textit{flex}} +\def\rup{r^\uparrow} +\def\retrieve{\textit{retrieve}} +\def\AALTS{\textit{AALTS}} +\def\AONE{\textit{AONE}} +%\theoremstyle{theorem} +%\newtheorem{theorem}{Theorem} +%\theoremstyle{lemma} +%\newtheorem{lemma}{Lemma} +%\newcommand{\lemmaautorefname}{Lemma} +%\theoremstyle{definition} +%\newtheorem{definition}{Definition} +\algnewcommand\algorithmicswitch{\textbf{switch}} +\algnewcommand\algorithmiccase{\textbf{case}} +\algnewcommand\algorithmicassert{\texttt{assert}} +\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}% +% New "environments" +\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}% +\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}% +\algtext*{EndSwitch}% +\algtext*{EndCase}% + + +\begin{document} + +\maketitle + +\begin{abstract} + Brzozowski introduced in 1964 a beautifully simple algorithm for + regular expression matching based on the notion of derivatives of + regular expressions. In 2014, Sulzmann and Lu extended this + algorithm to not just give a YES/NO answer for whether or not a + regular expression matches a string, but in case it does also + answers with \emph{how} it matches the string. This is important for + applications such as lexing (tokenising a string). The problem is to + make the algorithm by Sulzmann and Lu fast on all inputs without + breaking its correctness. Being fast depends on a complete set of + simplification rules, some of which + have been put forward by Sulzmann and Lu. We have extended their + rules in order to obtain a tight bound on the size of regular expressions. + We have tested these extended rules, but have not + formally established their correctness. We have also not yet looked + at extended regular expressions, such as bounded repetitions, + negation and back-references. +\end{abstract} + +\section{Recapitulation of Concepts From the Last Report} + +\subsection*{Regular Expressions and Derivatives} + +Suppose (basic) regular expressions are given by the following grammar: + +\[ r ::= \ZERO \mid \ONE + \mid c + \mid r_1 \cdot r_2 + \mid r_1 + r_2 + \mid r^* +\] + +\noindent +The ingenious contribution of Brzozowski is the notion of \emph{derivatives} of +regular expressions, written~$\_ \backslash \_$. It uses the auxiliary notion of +$\nullable$ defined below. + +\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} + +\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} + +%Assuming the classic notion of a +%\emph{language} of a regular expression, written $L(\_)$, t + +\noindent +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 +We can generalise the derivative operation shown above for single characters +to strings as follows: + +\begin{center} +\begin{tabular}{lcl} +$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\ +$r \backslash [\,] $ & $\dn$ & $r$ +\end{tabular} +\end{center} + +\noindent +and then define Brzozowski's regular-expression matching algorithm as: + +\[ +match\;s\;r \;\dn\; nullable(r\backslash s) +\] + +\noindent +Assuming the a string is givane as a sequence of characters, say $c_0c_1..c_n$, +this algorithm presented graphically is as follows: + +\begin{equation}\label{graph:*} +\begin{tikzcd} +r_0 \arrow[r, "\backslash c_0"] & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed] & r_n \arrow[r,"\textit{nullable}?"] & \;\textrm{YES}/\textrm{NO} +\end{tikzcd} +\end{equation} + +\noindent +where we start with a regular expression $r_0$, build successive +derivatives until we exhaust the string and then use \textit{nullable} +to test whether the result can match the empty string. It can be +relatively easily shown that this matcher is correct (that is given +an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$). + + +\subsection*{Values and the Lexing Algorithm by Sulzmann and Lu} + +One limitation 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} or +sometimes also \emph{lexical value}. These values and regular +expressions correspond to each other as illustrated in the following +table: + + +\begin{center} + \begin{tabular}{c@{\hspace{20mm}}c} + \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} + & + \begin{tabular}{@{\hspace{0mm}}rrl@{}} + \multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\ + $v$ & $::=$ & \\ + & & $\Empty$ \\ + & $\mid$ & $\Char(c)$ \\ + & $\mid$ & $\Seq\,v_1\, v_2$\\ + & $\mid$ & $\Left(v)$ \\ + & $\mid$ & $\Right(v)$ \\ + & $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\ + \end{tabular} + \end{tabular} +\end{center} + +\noindent +The contribution of Sulzmann and Lu is an extension of Brzozowski's +algorithm by a second phase (the first phase being building successive +derivatives---see \eqref{graph:*}). In this second phase, a POSIX value +is generated in case the regular expression matches the string. +Pictorially, the Sulzmann and Lu algorithm is as follows: + +\begin{ceqn} +\begin{equation}\label{graph:2} +\begin{tikzcd} +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} +\end{equation} +\end{ceqn} + +\noindent +For convenience, we shall employ the following notations: the regular +expression we start with is $r_0$, and the given string $s$ is composed +of characters $c_0 c_1 \ldots c_{n-1}$. In the first phase from the +left to right, we build the derivatives $r_1$, $r_2$, \ldots according +to the characters $c_0$, $c_1$ until we exhaust the string and obtain +the derivative $r_n$. We test whether this derivative is +$\textit{nullable}$ or not. If not, we know the string does not match +$r$ and no value needs to be generated. If yes, we start building the +values incrementally by \emph{injecting} back the characters into the +earlier values $v_n, \ldots, v_0$. This is the second phase of the +algorithm from the right to left. For the first value $v_n$, we call the +function $\textit{mkeps}$, which builds the lexical value +for how the empty string has been matched by the (nullable) regular +expression $r_n$. This function is defined as + + \begin{center} + \begin{tabular}{lcl} + $\mkeps(\ONE)$ & $\dn$ & $\Empty$ \\ + $\mkeps(r_{1}+r_{2})$ & $\dn$ + & \textit{if} $\nullable(r_{1})$\\ + & & \textit{then} $\Left(\mkeps(r_{1}))$\\ + & & \textit{else} $\Right(\mkeps(r_{2}))$\\ + $\mkeps(r_1\cdot r_2)$ & $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\ + $mkeps(r^*)$ & $\dn$ & $\Stars\,[]$ + \end{tabular} + \end{center} + + +\noindent +After the $\mkeps$-call, we inject back the characters one by one in order to build +the lexical value $v_i$ for how the regex $r_i$ matches the string $s_i$ +($s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$. +After injecting back $n$ characters, we get the lexical value for how $r_0$ +matches $s$. For this Sulzmann and Lu defined a function that reverses +the ``chopping off'' of characters during the derivative phase. The +corresponding function is called \emph{injection}, written +$\textit{inj}$; it takes three arguments: the first one is a regular +expression ${r_{i-1}}$, before the character is chopped off, the second +is a character ${c_{i-1}}$, the character we want to inject and the +third argument is the value ${v_i}$, into which one wants to inject the +character (it corresponds to the regular expression after the character +has been chopped off). The result of this function is a new value. The +definition of $\textit{inj}$ is as follows: + +\begin{center} +\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l} + $\textit{inj}\,(c)\,c\,Empty$ & $\dn$ & $Char\,c$\\ + $\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\ + $\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\ + $\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\ + $\textit{inj}\,(r_1 \cdot r_2)\,c\,\Left(Seq(v_1,v_2))$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\ + $\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$ & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\ + $\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$ & $\dn$ & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\ +\end{tabular} +\end{center} + +\noindent This definition is by recursion on the ``shape'' of regular +expressions and values. + + +\subsection*{Simplification of Regular Expressions} + +The main drawback of building successive derivatives according +to Brzozowski's definition is that they can grow very quickly in size. +This is mainly due to the fact that the derivative operation generates +often ``useless'' $\ZERO$s and $\ONE$s in derivatives. As a result, if +implemented naively both algorithms by Brzozowski and by Sulzmann and Lu +are excruciatingly slow. For example when starting with the regular +expression $(a + aa)^*$ and building 12 successive derivatives +w.r.t.~the character $a$, one obtains a derivative regular expression +with more than 8000 nodes (when viewed as a tree). Operations like +$\textit{der}$ and $\nullable$ need to traverse such trees and +consequently the bigger the size of the derivative the slower the +algorithm. + +Fortunately, one can simplify regular expressions after each derivative +step. Various simplifications of regular expressions are possible, such +as the simplification of $\ZERO + r$, $r + \ZERO$, $\ONE\cdot r$, $r +\cdot \ONE$, and $r + r$ to just $r$. These simplifications do not +affect the answer for whether a regular expression matches a string or +not, but fortunately also do not affect the POSIX strategy of how +regular expressions match strings---although the latter is much harder +to establish. Some initial results in this regard have been +obtained in \cite{AusafDyckhoffUrban2016}. + +If we want the size of derivatives in Sulzmann and Lu's algorithm to +stay below this bound, we would need more aggressive simplifications. +Essentially we need to delete useless $\ZERO$s and $\ONE$s, as well as +deleting duplicates whenever possible. For example, the parentheses in +$(a+b) \cdot c + b\cdot c$ can be opened up to get $a\cdot c + b \cdot c + b +\cdot c$, and then simplified to just $a \cdot c + b \cdot c$. Another +example is simplifying $(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to just +$a^*+a+\ONE$. Adding these more aggressive simplification rules help us +to achieve the same size bound as that of the partial derivatives. + +In order to implement the idea of ``spilling out alternatives'' and to +make them compatible with the $\textit{inj}$-mechanism, we use +\emph{bitcodes}. They were first introduced by Sulzmann and Lu. +Here bits and bitcodes (lists of bits) are defined as: + +\begin{center} + $b ::= 1 \mid 0 \qquad +bs ::= [] \mid b:bs +$ +\end{center} + +\noindent +The $1$ and $0$ are not in bold in order to avoid +confusion with the regular expressions $\ZERO$ and $\ONE$. Bitcodes (or +bit-lists) can be used to encode values (or incomplete values) in a +compact form. This can be straightforwardly seen in the following +coding function from values to bitcodes: + +\begin{center} +\begin{tabular}{lcl} + $\textit{code}(\Empty)$ & $\dn$ & $[]$\\ + $\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\ + $\textit{code}(\Left\,v)$ & $\dn$ & $0 :: code(v)$\\ + $\textit{code}(\Right\,v)$ & $\dn$ & $1 :: code(v)$\\ + $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\ + $\textit{code}(\Stars\,[])$ & $\dn$ & $[0]$\\ + $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $1 :: code(v) \;@\; + code(\Stars\,vs)$ +\end{tabular} +\end{center} + +\noindent +Here $\textit{code}$ encodes a value into a bitcodes by converting +$\Left$ into $0$, $\Right$ into $1$, and marks the start of a non-empty +star iteration by $1$. The border where a local star terminates +is marked by $0$. This coding is lossy, as it throws away the information about +characters, and also does not encode the ``boundary'' between two +sequence values. Moreover, with only the bitcode we cannot even tell +whether the $1$s and $0$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 manipulated and ``moved +around'' in a regular expression. In order to recover values, we will +need the corresponding regular expression as an extra information. This +means the decoding function is defined as: + + +%\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}'\,(0\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & + $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\; + (\Left\,v, bs_1)$\\ + $\textit{decode}'\,(1\!::\!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}'\,(0\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ + $\textit{decode}'\,(1\!::\!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} + +Sulzmann and Lu's integrated the bitcodes into regular expressions to +create annotated regular expressions \cite{Sulzmann2014}. +\emph{Annotated regular expressions} are defined by the following +grammar:%\comment{ALTS should have an $as$ in the definitions, not just $a_1$ and $a_2$} + +\begin{center} +\begin{tabular}{lcl} + $\textit{a}$ & $::=$ & $\ZERO$\\ + & $\mid$ & $_{bs}\ONE$\\ + & $\mid$ & $_{bs}{\bf c}$\\ + & $\mid$ & $_{bs}\oplus\,as$\\ + & $\mid$ & $_{bs}a_1\cdot a_2$\\ + & $\mid$ & $_{bs}a^*$ +\end{tabular} +\end{center} +%(in \textit{ALTS}) + +\noindent +where $bs$ stands for bitcodes, $a$ for $\bold{a}$nnotated regular +expressions and $as$ for a list of annotated regular expressions. +The alternative constructor($\oplus$) has been generalized to +accept a list of annotated regular expressions rather than just 2. +We will show that these bitcodes encode information about +the (POSIX) value that should be generated by the Sulzmann and Lu +algorithm. + + +To do lexing using annotated regular expressions, we shall first +transform the usual (un-annotated) regular expressions into annotated +regular expressions. This operation is called \emph{internalisation} and +defined as follows: + +%\begin{definition} +\begin{center} +\begin{tabular}{lcl} + $(\ZERO)^\uparrow$ & $\dn$ & $\ZERO$\\ + $(\ONE)^\uparrow$ & $\dn$ & $_{[]}\ONE$\\ + $(c)^\uparrow$ & $\dn$ & $_{[]}{\bf c}$\\ + $(r_1 + r_2)^\uparrow$ & $\dn$ & + $_{[]}\oplus[\textit{fuse}\,[0]\,r_1^\uparrow,\, + \textit{fuse}\,[1]\,r_2^\uparrow]$\\ + $(r_1\cdot r_2)^\uparrow$ & $\dn$ & + $_{[]}r_1^\uparrow \cdot r_2^\uparrow$\\ + $(r^*)^\uparrow$ & $\dn$ & + $_{[]}(r^\uparrow)^*$\\ +\end{tabular} +\end{center} +%\end{definition} + +\noindent +We use up arrows here to indicate that the basic un-annotated regular +expressions are ``lifted up'' into something slightly more complex. In the +fourth clause, $\textit{fuse}$ is an auxiliary function that helps to +attach bits to the front of an annotated regular expression. Its +definition is as follows: + +\begin{center} +\begin{tabular}{lcl} + $\textit{fuse}\;bs \; \ZERO$ & $\dn$ & $\ZERO$\\ + $\textit{fuse}\;bs\; _{bs'}\ONE$ & $\dn$ & + $_{bs @ bs'}\ONE$\\ + $\textit{fuse}\;bs\;_{bs'}{\bf c}$ & $\dn$ & + $_{bs@bs'}{\bf c}$\\ + $\textit{fuse}\;bs\,_{bs'}\oplus\textit{as}$ & $\dn$ & + $_{bs@bs'}\oplus\textit{as}$\\ + $\textit{fuse}\;bs\; _{bs'}a_1\cdot a_2$ & $\dn$ & + $_{bs@bs'}a_1 \cdot a_2$\\ + $\textit{fuse}\;bs\,_{bs'}a^*$ & $\dn$ & + $_{bs @ bs'}a^*$ +\end{tabular} +\end{center} + +\noindent +After internalising the regular expression, we perform successive +derivative operations on the annotated regular expressions. This +derivative operation is the same as what we had previously for the +basic regular expressions, except that we beed to take care of +the bitcodes: + + +\iffalse + %\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{ALTS}\;bs\,as)\,\backslash c$ & $\dn$ & + $\textit{ALTS}\;bs\,(as.map(\backslash c))$\\ + $(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ & + $\textit{if}\;\textit{bnullable}\,a_1$\\ + & &$\textit{then}\;\textit{ALTS}\,bs\,List((\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\ + & &$\phantom{\textit{then}\;\textit{ALTS}\,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} + +\begin{center} + \begin{tabular}{@{}lcl@{}} + $(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ + $(_{bs}\textit{ONE})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ + $(_{bs}\textit{CHAR}\;d)\,\backslash c$ & $\dn$ & + $\textit{if}\;c=d\; \;\textit{then}\; + _{bs}\textit{ONE}\;\textit{else}\;\textit{ZERO}$\\ + $(_{bs}\textit{ALTS}\;\textit{as})\,\backslash c$ & $\dn$ & + $_{bs}\textit{ALTS}\;(\textit{as}.\textit{map}(\backslash c))$\\ + $(_{bs}\textit{SEQ}\;a_1\,a_2)\,\backslash c$ & $\dn$ & + $\textit{if}\;\textit{bnullable}\,a_1$\\ + & &$\textit{then}\;_{bs}\textit{ALTS}\,List((_{[]}\textit{SEQ}\,(a_1\,\backslash c)\,a_2),$\\ + & &$\phantom{\textit{then}\;_{bs}\textit{ALTS}\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\ + & &$\textit{else}\;_{bs}\textit{SEQ}\,(a_1\,\backslash c)\,a_2$\\ + $(_{bs}\textit{STAR}\,a)\,\backslash c$ & $\dn$ & + $_{bs}\textit{SEQ}\;(\textit{fuse}\, [0] \; r\,\backslash c )\, + (_{bs}\textit{STAR}\,[]\,r)$ +\end{tabular} +\end{center} +%\end{definition} +\fi + +\begin{center} + \begin{tabular}{@{}lcl@{}} + $(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\ + $(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\ + $(_{bs}{\bf d})\,\backslash c$ & $\dn$ & + $\textit{if}\;c=d\; \;\textit{then}\; + _{bs}\ONE\;\textit{else}\;\ZERO$\\ + $(_{bs}\oplus \;\textit{as})\,\backslash c$ & $\dn$ & + $_{bs}\oplus\;(\textit{as.map}(\backslash c))$\\ + $(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ & + $\textit{if}\;\textit{bnullable}\,a_1$\\ + & &$\textit{then}\;_{bs}\oplus\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\ + & &$\phantom{\textit{then},\;_{bs}\oplus\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\ + & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\ + $(_{bs}a^*)\,\backslash c$ & $\dn$ & + $_{bs}(\textit{fuse}\, [0] \; r\,\backslash c)\cdot + (_{[]}r^*))$ +\end{tabular} +\end{center} + +%\end{definition} +\noindent +For instance, when we do derivative of $_{bs}a^*$ with respect to c, +we need to unfold it into a sequence, +and attach an additional bit $0$ to the front of $r \backslash c$ +to indicate that there is one more star iteration. Also the sequence clause +is more subtle---when $a_1$ is $\textit{bnullable}$ (here +\textit{bnullable} is exactly the same as $\textit{nullable}$, except +that it is for annotated regular expressions, therefore we omit the +definition). Assume that $\textit{bmkeps}$ correctly extracts the bitcode for how +$a_1$ matches the string prior to character $c$ (more on this later), +then the right branch of alternative, which is $\textit{fuse} \; \bmkeps \; a_1 (a_2 +\backslash c)$ will collapse the regular expression $a_1$(as it has +already been fully matched) and store the parsing information at the +head of the regular expression $a_2 \backslash c$ by fusing to it. The +bitsequence $\textit{bs}$, which was initially attached to the +first element of the sequence $a_1 \cdot a_2$, has +now been elevated to the top-level of $\oplus$, as this information will be +needed whichever way the sequence is matched---no matter whether $c$ belongs +to $a_1$ or $ a_2$. After building these derivatives and maintaining all +the lexing information, we complete the lexing by collecting the +bitcodes using a generalised version of the $\textit{mkeps}$ function +for annotated regular expressions, called $\textit{bmkeps}$: + + +%\begin{definition}[\textit{bmkeps}]\mbox{} +\begin{center} +\begin{tabular}{lcl} + $\textit{bmkeps}\,(_{bs}\ONE)$ & $\dn$ & $bs$\\ + $\textit{bmkeps}\,(_{bs}\oplus a::\textit{as})$ & $\dn$ & + $\textit{if}\;\textit{bnullable}\,a$\\ + & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ + & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\oplus \textit{as})$\\ + $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ & + $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ + $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ & + $bs \,@\, [0]$ +\end{tabular} +\end{center} +%\end{definition} + +\noindent +This function completes the value information by travelling along the +path of the regular expression that corresponds to a POSIX value and +collecting all the bitcodes, and using $S$ to indicate the end of star +iterations. If we take the bitcodes produced by $\textit{bmkeps}$ and +decode them, we get the value we expect. The corresponding lexing +algorithm looks as follows: + +\begin{center} +\begin{tabular}{lcl} + $\textit{blexer}\;r\,s$ & $\dn$ & + $\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\ + & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ + & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ + & & $\;\;\textit{else}\;\textit{None}$ +\end{tabular} +\end{center} + +\noindent +In this definition $\_\backslash s$ is the generalisation of the derivative +operation from characters to strings (just like the derivatives for un-annotated +regular expressions). + + +\subsection*{Our Simplification Rules} + +The main point of the bitcodes 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 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 many regular +expressions and strings. + +One modification we introduced is to allow a list of annotated regular +expressions in the $\oplus$ constructor. This allows us to not just +delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but +also unnecessary ``copies'' of regular expressions (very similar to +simplifying $r + r$ to just $r$, but in a more general setting). 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 subsequent copies can be pruned away from +the regular expression. A recursive definition of our simplification function +that looks somewhat similar to our Scala code is given below: +%\comment{Use $\ZERO$, $\ONE$ and so on. +%Is it $ALTS$ or $ALTS$?}\\ + +\begin{center} + \begin{tabular}{@{}lcl@{}} + + $\textit{simp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ + &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ + &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ + &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow _{bs}a_1' \cdot a_2'$ \\ + + $\textit{simp} \; (_{bs}\oplus \textit{as})$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ + &&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ + &&$\quad\textit{case} \; as' \Rightarrow _{bs}\oplus \textit{as'}$\\ + + $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ +\end{tabular} +\end{center} + +\noindent +The simplification does a pattern matching on the regular expression. +When it detected that the regular expression is an alternative or +sequence, it will try to simplify its children regular expressions +recursively and then see if one of the children turn into $\ZERO$ or +$\ONE$, which might trigger further simplification at the current level. +The most involved part is the $\oplus$ clause, where we use two +auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested +alternatives and reduce as many duplicates as possible. Function +$\textit{distinct}$ keeps the first occurring copy only and remove all later ones +when detected duplicates. Function $\textit{flatten}$ opens up nested $\oplus$s. +Its recursive definition is given below: + + \begin{center} + \begin{tabular}{@{}lcl@{}} + $\textit{flatten} \; (_{bs}\oplus \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \; + (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\ + $\textit{flatten} \; \ZERO :: as'$ & $\dn$ & $ \textit{flatten} \; \textit{as'} $ \\ + $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; \textit{as'}$ \quad(otherwise) +\end{tabular} +\end{center} + +\noindent +Here $\textit{flatten}$ behaves like the traditional functional programming flatten +function, except that it also removes $\ZERO$s. Or in terms of regular expressions, it +removes parentheses, for example changing $a+(b+c)$ into $a+b+c$. + +Suppose we apply simplification after each derivative step, and view +these two operations as an atomic one: $a \backslash_{simp}\,c \dn +\textit{simp}(a \backslash c)$. Then we can use the previous natural +extension from derivative w.r.t.~character to derivative +w.r.t.~string:%\comment{simp in the [] case?} + +\begin{center} +\begin{tabular}{lcl} +$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp}\, c) \backslash_{simp}\, s$ \\ +$r \backslash_{simp} [\,] $ & $\dn$ & $r$ +\end{tabular} +\end{center} + +\noindent +we obtain an optimised version of the algorithm: + + \begin{center} +\begin{tabular}{lcl} + $\textit{blexer\_simp}\;r\,s$ & $\dn$ & + $\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\ + & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ + & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ + & & $\;\;\textit{else}\;\textit{None}$ +\end{tabular} +\end{center} + +\noindent +This algorithm keeps the regular expression size small, for example, +with this simplification our previous $(a + aa)^*$ example's 8000 nodes +will be reduced to just 6 and stays constant, no matter how long the +input string is. + + + +\section{Introduction} + +While we believe derivatives of regular expressions, written +$r\backslash s$, are a beautiful concept (in terms of ease of +implementing them in functional programming languages and in terms of +reasoning about them formally), they have one major drawback: every +derivative step can make regular expressions grow drastically in +size. This in turn has negative effect on the runtime of the +corresponding lexing algorithms. Consider for example the regular +expression $(a+aa)^*$ and the short string $aaaaaaaaaaaa$. The +corresponding derivative contains already 8668 nodes where we assume +the derivative is given as a tree. The reason for the poor runtime of +the derivative-based lexing algorithms is that they need to traverse +such trees over and over again. The solution is to find a complete set +of simplification rules that keep the sizes of derivatives uniformly +small. + +For reasons beyond this report, it turns out that a complete set of +simplification rules depends on values being encoded as +bitsequences.\footnote{Values are the results the lexing algorithms + generate; they encode how a regular expression matched a string.} We +already know that the lexing algorithm using bitsequences but +\emph{without} simplification is correct, albeilt horribly +slow. Therefore in the past 6 months I was trying to prove that the +algorithm using bitsequences plus our simplification rules is +also correct. Formally this amounts to show that + +\begin{equation}\label{mainthm} +\blexers \; r \; s = \blexer \;r\;s +\end{equation} + +\noindent +whereby $\blexers$ simplifies (makes derivatives smaller) in each +step, whereas with $\blexer$ the size can grow exponentially. This +would be an important milestone for my thesis, because we already +have a very good idea how to establish that our set our simplification +rules keeps the size of derivativs below a relatively tight bound. + +In order to prove the main theorem in \eqref{mainthm}, we need to prove that the +two functions produce the same output. The definition of these two functions +is shown below. + +\begin{center} +\begin{tabular}{lcl} + $\textit{blexer}\;r\,s$ & $\dn$ & + $\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\ + & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ + & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ + & & $\;\;\textit{else}\;\textit{None}$ +\end{tabular} +\end{center} + +\begin{center} +\begin{tabular}{lcl} + $\blexers \; r \, s$ &$\dn$ & + $\textit{let} \; a = (r^\uparrow)\backslash_{simp}\, s\; \textit{in}$\\ + & & $\; \; \textit{if} \; \textit{bnullable}(a)$\\ + & & $\; \; \textit{then} \; \textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ + & & $\;\; \textit{else}\;\textit{None}$ +\end{tabular} +\end{center} +\noindent +In these definitions $(r^\uparrow)$ is a kind of coding function that +is the same in each case, similarly the decode and the \textit{bmkeps} +are functions that are the same in each case. Our main +theorem~\eqref{mainthm} therefore boils down to proving the following +two propositions (depending on which branch the if-else clause +takes). They establish how the derivatives \emph{with} simplification +do not change the computed result: + +\begin{itemize} +\item{(a)} If a string $s$ is in the language of $L(r)$, then \\ +$\textit{bmkeps} (r^\uparrow)\backslash_{simp}\,s = \textit{bmkeps} (r^\uparrow)\backslash s$,\\ +\item{(b)} If a string $s$ is in the language $L(r)$, then +$\rup \backslash_{simp} \,s$ is not nullable. +\end{itemize} + +\noindent +We have already proved the second part in Isabelle. This is actually +not too difficult because we can show that simplification does not +change the language of simplified regular expressions. + +If we can prove the first part, that is the bitsequence algorithm with +simplification produces the same result as the one without +simplification, then we are done. Unfortunately that part requires +more effort, because simplification does not only need to \emph{not} +change the language, but also not change the value (that is the +computed result). + +%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt} +%Do you want to keep this? You essentially want to say that the old +%method used retrieve, which unfortunately cannot be adopted to +%the simplification rules. You could just say that and give an example. +%However you have to think about how you give the example....nobody knows +%about AZERO etc yet. Maybe it might be better to use normal regexes +%like $a + aa$, but annotate bitsequences as subscript like $_1(_0a + _1aa)$. + +%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt} +%REPLY:\\ +%Yes, I am essentially saying that the old method +%cannot be adopted without adjustments. +%But this does not mean we should skip +%the proof of the bit-coded algorithm +%as it is still the main direction we are looking into +%to prove things. We are trying to modify +%the old proof to suit our needs, but not give +%up it totally, that is why i believe the old +%proof is fundamental in understanding +%what we are doing in the past 6 months. +%\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt} + +\subsubsection*{Existing Proof} + +For this we have started with looking at the original proof that +established that the bitsequence algorrithm produces the same result +as the algorithm not using bitsequences. Formally this proof +established + +\begin{equation}\label{lexer} +\blexer \; (r^\uparrow) s = \lexer \;r \;s +\end{equation} + +%\noindent +%might provide us insight into proving +%\begin{center} +%$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$ +%\end{center} + +\noindent +The proof uses two ``tricks''. One is that it uses a \flex-function + +\begin{center} +\begin{tabular}{lcl} +$\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\ +$\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$ +\end{tabular} +\end{center} + +\noindent +and then proves for the right-hand side in \eqref{lexer} + +\begin{center} +$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$ +\end{center}. + + + + +\noindent +The $\flex$-function essentially does lexing by +stacking up injection functions while doing derivatives. + +explicitly showing the order of characters being +injected back in each step. +With $\flex$ we can write $\lexer$ this way: + +\begin{center} +$\lexer \;r\; s = \flex \;id \; r\;s \;(\mkeps r\backslash s)$ +\end{center} + +%\noindent +%$\flex$ focuses on the injections instead of the derivatives , +%compared to the original definition of $\lexer$, which puts equal +%amount of emphasis on injection and derivative with respect to each +%character: + +%\begin{center} +%\begin{tabular}{lcl} +%$\textit{lexer} \; r\; (c\!::\!s) $ & $\dn$ & $\textit{case} \; \lexer \; (r\backslash c) \;s \; %\textit{of}$ \\ +% & & $\textit{None} \; \Longrightarrow \; \textit{None}$\\ +% & & $\textbar \; v \; \Longrightarrow \; \inj \; r\;c\;v$\\ +%$\textit{lexer} \; r\; [\,] $ & $\dn$ & $\textit{if} \; \nullable (r) \; \textit{then} \; \mkeps% (r) \; \textit{else} \;None$ +%\end{tabular} +%\end{center} + +\noindent +The crux in the existing proof is how $\flex$ relates to injection, namely + +\begin{center} +$\flex \; r \; id \; (s@[c]) \; v = \flex \; r \; id \; s \; (inj \; (r\backslash s) \; c\; v)$. +\end{center} + +\noindent +This property allows one to rewrite an induction hypothesis like + +\begin{center} +$ \flex \; r\; id\; (s@[c])\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$ +\end{center} + + +\subsubsection{Retrieve Function} +The crucial point is to find the +$\textit{POSIX}$ information of a regular expression and how it is modified, +augmented and propagated +during simplification in parallel with the regular expression that +has not been simplified in the subsequent derivative operations. To aid this, +we use the helper function retrieve described by Sulzmann and Lu: +\begin{center} +\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}} + $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\ + $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\ + $\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Left\,v)$ & $\dn$ & + $bs \,@\, \textit{retrieve}\,a\,v$\\ + $\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Right\,v)$ & $\dn$ & + $\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\oplus as)\,v$\\ + $\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ & + $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\ + $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ & + $bs \,@\, [0]$\\ + $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\ + \multicolumn{3}{l}{ + \hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\, + \textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\ +\end{tabular} +\end{center} +%\comment{Did not read further}\\ +This function assembles the bitcode +%that corresponds to a lexical value for how +%the current derivative matches the suffix of the string(the characters that +%have not yet appeared, but will appear as the successive derivatives go on. +%How do we get this "future" information? By the value $v$, which is +%computed by a pass of the algorithm that uses +%$inj$ as described in the previous section). +using information from both the derivative regular expression and the +value. Sulzmann and Lu poroposed this function, but did not prove +anything about it. Ausaf and Urban used it to connect the bitcoded +algorithm to the older algorithm by the following equation: + + \begin{center} $inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\; + (r^\uparrow)\backslash_{simp} \,c)\,v)$ + \end{center} + +\noindent +whereby $r^\uparrow$ stands for the internalised version of $r$. Ausaf +and Urban also used this fact to prove the correctness of bitcoded +algorithm without simplification. Our purpose of using this, however, +is to establish + +\begin{center} +$ \textit{retrieve} \; +a \; v \;=\; \textit{retrieve} \; (\textit{simp}\,a) \; v'.$ +\end{center} +The idea is that using $v'$, a simplified version of $v$ that had gone +through the same simplification step as $\textit{simp}(a)$, we are able +to extract the bitcode that gives the same parsing information as the +unsimplified one. However, we noticed that constructing such a $v'$ +from $v$ is not so straightforward. The point of this is that we might +be able to finally bridge the gap by proving + +\noindent +By using a property of retrieve we have the $\textit{RHS}$ of the above equality is +$decode (retrieve (r^\uparrow \backslash(s @ [c])) v) r$, and this gives the +main lemma result: + +\begin{center} +$ \flex \;r\; id \; (s@[c]) \; v =\textit{decode}(\textit{retrieve} (\rup \backslash (s@[c])) \;v) r$ +\end{center} + + + + +\noindent +To use this lemma result for our +correctness proof, simply replace the $v$ in the +$\textit{RHS}$ of the above equality with +$\mkeps\;(r\backslash (s@[c]))$, and apply the lemma that + +\begin{center} +$\textit{decode} \; \bmkeps \; \rup \; r = \textit{decode} \; (\textit{retrieve} \; \rup \; \mkeps(r)) \;r$ +\end{center} +\noindent +We get the correctness of our bit-coded algorithm: +\begin{center} +$\flex \;r\; id \; s \; (\mkeps \; r\backslash s) = \textit{decode} \; \bmkeps \; \rup\backslash s \; r$ +\end{center} +\noindent +The bridge between the above chain of equalities +is the use of $\retrieve$, +if we want to use a similar technique for the +simplified version of algorithm, +we face the problem that in the above +equalities, +$\retrieve \; a \; v$ is not always defined. +for example, +$\retrieve \; _0(_1a+_0a) \; \Left(\Empty)$ +is defined, but not $\retrieve \; (_{01}a) \;\Left(\Empty)$, +though we can extract the same POSIX +bits from the two annotated regular expressions. +The latter might occur when we try to retrieve from +a simplified regular expression using the same value +as the unsimplified one. +This is because $\Left(\Empty)$ corresponds to +the regular expression structure $\ONE+r_2$ instead of +$\ONE$. +That means, if we +want to prove that +\begin{center} +$\textit{decode} \; \bmkeps \; \rup\backslash s \; r = \textit{decode} \; \bmkeps \; \rup\backslash_{simp} s \; r$ +\end{center} +\noindent +holds by using $\retrieve$, +we probably need to prove an equality like below: +\begin{center} +%$\retrieve \; \rup\backslash_{simp} s \; \mkeps(r\backslash_{simp} s)=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$ +$\retrieve \; \rup\backslash_{simp} s \; \mkeps(f(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$ +\end{center} +\noindent +$f$ rectifies $r\backslash s$ so the value $\mkeps(f(r\backslash s))$ becomes + something simpler +to make the retrieve function defined.\\ +\subsubsection{Ways to Rectify Value} +One way to do this is to prove the following: +\begin{center} +$\retrieve \; \rup\backslash_{simp} s \; \mkeps(\simp(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$ +\end{center} +\noindent +The reason why we choose $\simp$ as $f$ is because +$\rup\backslash_{simp} \, s$ and $\simp(\rup\backslash \, s)$ +have the same shape: +\begin{center} +$\erase (\rup\backslash_{simp} \, s) = \erase(\simp(\rup\backslash s))$ +\end{center} + +\noindent +$\erase$ in the above equality means to remove the bit-codes +in an annotated regular expression and only keep the original +regular expression(just like "erasing" the bits). Its definition is omitted. +$\rup\backslash_{simp} \, s$ and $\simp(\rup\backslash s)$ +are very closely related, but not identical. +\subsubsection{Example for $\rup\backslash_{simp} \, s \neq \simp(\rup\backslash s)$} +For example, let $r$ be the regular expression +$(a+b)(a+a*)$ and $s$ be the string $aa$, then +both $\erase (\rup\backslash_{simp} \, s)$ and $\erase (\simp (\rup\backslash s))$ +are $\ONE + a^*$. However, without $\erase$ +\begin{center} +$\rup\backslash_{simp} \, s$ is equal to $_0(_0\ONE +_{11}a^*)$ +\end{center} +\noindent +whereas +\begin{center} +$\simp(\rup\backslash s)$ is equal to $(_{00}\ONE +_{011}a^*)$ +\end{center} +\noindent +(For the sake of visual simplicity, we use numbers to denote the bits +in bitcodes as we have previously defined for annotated +regular expressions. $\S$ is replaced by +subscript $_1$ and $\Z$ by $_0$.) + +What makes the difference? + +%Two "rules" might be inferred from the above example. + +%First, after erasing the bits the two regular expressions +%are exactly the same: both become $1+a^*$. Here the +%function $\simp$ exhibits the "one in the end equals many times +%at the front" +%property: one simplification in the end causes the +%same regular expression structure as +%successive simplifications done alongside derivatives. +%$\rup\backslash_{simp} \, s$ unfolds to +%$\simp((\simp(r\backslash a))\backslash a)$ +%and $\simp(\rup\backslash s)$ unfolds to +%$\simp((r\backslash a)\backslash a)$. The one simplification +%in the latter causes the resulting regular expression to +%become $1+a^*$, exactly the same as the former with +%two simplifications. + +%Second, the bit-codes are different, but they are essentially +%the same: if we push the outmost bits ${\bf_0}(_0\ONE +_{11}a^*)$ of $\rup\backslash_{simp} \, s$ +%inside then we get $(_{00}\ONE +_{011}a^*)$, exactly the +%same as that of $\rup\backslash \, s$. And this difference +%does not matter when we try to apply $\bmkeps$ or $\retrieve$ +%to it. This seems a good news if we want to use $\retrieve$ +%to prove things. + +%If we look into the difference above, we could see that the +%difference is not fundamental: the bits are just being moved +%around in a way that does not hurt the correctness. +During the first derivative operation, +$\rup\backslash a=(_0\ONE + \ZERO)(_0a + _1a^*)$ is +in the form of a sequence regular expression with +two components, the first +one $\ONE + \ZERO$ being nullable. +Recall the simplification function definition: +\begin{center} + \begin{tabular}{@{}lcl@{}} + + $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ + &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ + &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ + &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\ + + $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ + &&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ + &&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\ + + $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ +\end{tabular} +\end{center} + +\noindent + +and the difinition of $\flatten$: + \begin{center} + \begin{tabular}{c c c} + $\flatten \; []$ & $\dn$ & $[]$\\ + $\flatten \; \ZERO::rs$ & $\dn$ & $rs$\\ + $\flatten \;(_{\textit{bs}_1}\oplus \textit{rs}_1 ::rs)$ & $\dn$ & $(\map \, (\fuse \, \textit{bs}_1) \,\textit{rs}_1) ::: \flatten(rs)$\\ + $\flatten \; r :: rs$ & $\dn$ & $r::\flatten(rs)$ + \end{tabular} + \end{center} + + \noindent +If we call $\simp$ on $\rup\backslash a$, just as $\backslash_{simp}$ +requires, then we would go throught the third clause of +the sequence case:$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$. +The $\ZERO$ of $(_0\ONE + \ZERO)$ is thrown away +by $\flatten$ and +$_0\ONE$ merged into $(_0a + _1a^*)$ by simply +putting its bits($_0$) to the front of the second component: + ${\bf_0}(_0a + _1a^*)$. + After a second derivative operation, + namely, $(_0(_0a + _1a^*))\backslash a$, we get + $ + _0(_0 \ONE + _1(_1\ONE \cdot a^*)) + $, and this simplifies to $_0(_0 \ONE + _{11} a^*)$ + by the third clause of the alternative case: + $\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$. +The outmost bit $_0$ stays with +the outmost regular expression, rather than being fused to +its child regular expressions, as what we will later see happens +to $\simp(\rup\backslash \, s)$. +If we choose to not simplify in the midst of derivative operations, +but only do it at the end after the string has been exhausted, +namely, $\simp(\rup\backslash \, s)=\simp((\rup\backslash a)\backslash a)$, +then at the {\bf second} derivative of +$(\rup\backslash a)\bf{\backslash a}$ +we will go throught the clause of $\backslash$: +\begin{center} +\begin{tabular}{lcl} +$(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ & + $(when \; \textit{bnullable}\,a_1)$\\ + & &$\textit{ALTS}\,bs\,List(\;\;(\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\ + & &$(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))\;\;)$\\ +\end{tabular} +\end{center} + +because +$\rup\backslash a = (_0\ONE + \ZERO)(_0a + _1a^*)$ +is a sequence +with the first component being nullable +(unsimplified, unlike the first round of running$\backslash_{simp}$). +Therefore $((_0\ONE + \ZERO)(_0a + _1a^*))\backslash a$ splits into +$([(\ZERO + \ZERO)\cdot(_0a + _1a^*)] + _0( _0\ONE + _1[_1\ONE \cdot a^*]))$. +After these two successive derivatives without simplification, +we apply $\simp$ to this regular expression, which goes through +the alternative clause, and each component of +$([(\ZERO + \ZERO)\cdot(_0a + _1a^*)] + _0( _0\ONE + _1[_1\ONE \cdot a^*]))$ +will be simplified, giving us the list:$[\ZERO, _0(_0\ONE + _{11}a^*)]$ +This list is then "flattened"--$\ZERO$ will be +thrown away by $\textit{flatten}$; $ _0(_0\ONE + _{11}a^*)$ +is opened up to make the list consisting of two separate elements +$_{00}\ONE$ and $_{011}a^*$, note that $flatten$ +$\fuse$s the bit(s) $_0$ to the front of $_0\ONE $ and $_{11}a^*$. +The order of simplification, which impacts the order that alternatives +are opened up, causes +the bits to be moved differently. + + \subsubsection{A Failed Attempt To Remedy the Problem Above} +A simple class of regular expression and string +pairs $(r, s)$ can be deduced from the above example +which trigger the difference between +$\rup\backslash_{simp} \, s$ +and $\simp(\rup\backslash s)$: +\begin{center} +\begin{tabular}{lcl} +$D =\{ (r_1 \cdot r_2,\; [c_1c_2]) \mid $ & $\simp(r_2) = r_2, \simp(r_1 \backslash c_1) = \ONE,$\\ + $r_1 \; not \; \nullable, c_2 \in L(r_2),$ & $\exists \textit{rs},\textit{bs}.\; r_2 \backslash c_2 = _{bs}{\oplus rs}$\\ +$\exists \textit{rs}_1. \; \simp(r_2 \backslash c_2) = _{bs}{\oplus \textit{rs}_1}$ & $and \;\simp(r_1 \backslash [c_1c_2]) = \ZERO\}$\\ +\end{tabular} +\end{center} +We take a pair $(r, \;s)$ from the set $D$. + +Now we compute ${\bf \rup \backslash_{simp} s}$, we get: +\begin{center} +\begin{tabular}{lcl} +$(r_1\cdot r_2)\backslash_{simp} \, [c_1c_2]$ & $= \simp\left[ \big(\simp\left[ \left( r_1\cdot r_2 \right) \backslash c_1\right] \big)\backslash c_2\right]$\\ + & $= \simp\left[ \big(\simp \left[ \left(r_1 \backslash c_1\right) \cdot r_2 \right] \big) \backslash c_2 \right]$\\ + & $= \simp \left[ (\fuse \; \bmkeps(r_1\backslash c_1) \; \simp(r_2) ) \backslash c_2 \right]$,\\ + & $= \simp \left[ (\fuse \; \bmkeps(r_1\backslash c_1) \; r_2 ) \backslash c_2 \right]$, +\end{tabular} +\end{center} +\noindent +from the definition of $D$ we know $r_1 \backslash c_1$ is nullable, therefore +$\bmkeps(r_1\backslash c_1)$ returns a bitcode, we shall call it + $\textit{bs}_2$. +The above term can be rewritten as +\begin{center} +$ \simp \left[ \fuse \; \textit{bs}_2\; r_2 \backslash c_2 \right]$, +\end{center} +which is equal to +\begin{center} +$\simp \left[ \fuse \; \textit{bs}_2 \; _{bs}{\oplus rs} \right]$\\ +$=\simp \left[ \; _{bs_2++bs}{\oplus rs} \right]$\\ +$= \; _{bs_2++bs}{\oplus \textit{rs}_1} $ +\end{center} +\noindent +by using the properties from the set $D$ again +and again(The reason why we set so many conditions +that the pair $(r,s)$ need to satisfy is because we can +rewrite them easily to construct the difference.) + +Now we compute ${\bf \simp(\rup \backslash s)}$: +\begin{center} +$\simp \big[(r_1\cdot r_2) \backslash [c_1c_2] \big]= \simp \left[ ((r_1 \cdot r_2 )\backslash c_1) \backslash c_2 \right]$ +\end{center} +\noindent +Again, using the properties above, we obtain +the following chain of equalities: +\begin{center} +$\simp(\rup \backslash s)= \simp \left[ ((r_1 \cdot r_2 )\backslash c_1) \backslash c_2 \right]= \simp\left[ \left(r_1 \backslash c_1\right) \cdot r_2 \big) \backslash c_2 \right]$\\ +$= \simp \left[ \oplus[\big( \left(r_1 \backslash c_1\right) \backslash c_2 \big) \cdot r_2 \; , \; \fuse \; (\bmkeps \;r_1\backslash c_1) \; r_2 \backslash c_2 ] \right]$, +\end{center} +\noindent +as before, we call the bitcode returned by +$\bmkeps(r_1\backslash c_1)$ as +$\textit{bs}_2$. +Also, $\simp(r_2 \backslash c_2)$ is +$_{bs}\oplus \textit{rs}_1$, +and $( \left(r_1 \backslash c_1\right) \backslash c_2 \cdot r_2)$ +simplifies to $\ZERO$, +so the above term can be expanded as +\begin{center} +\begin{tabular}{l} +$\textit{distinct}(\flatten[\ZERO\;, \; _{\textit{bs}_2++\textit{bs}}\oplus \textit{rs}_1] ) \; \textit{match} $ \\ + $\textit{case} \; [] \Rightarrow \ZERO$ \\ + $\textit{case} \; a :: [] \Rightarrow \textit{\fuse \; \textit{bs} a}$ \\ + $\textit{case} \; as' \Rightarrow _{[]}\oplus as'$\\ +\end{tabular} +\end{center} +\noindent +Applying the definition of $\flatten$, we get +\begin{center} +$_{[]}\oplus (\textit{map} \; \fuse (\textit{bs}_2 ++ bs) rs_1)$ +\end{center} +\noindent +compared to the result +\begin{center} +$ \; _{bs_2++bs}{\oplus \textit{rs}_1} $ +\end{center} +\noindent +Note how these two regular expressions only +differ in terms of the position of the bits +$\textit{bs}_2++\textit{bs}$. They are the same otherwise. +What caused this difference to happen? +The culprit is the $\flatten$ function, which spills +out the bitcodes in the inner alternatives when +there exists an outer alternative. +Note how the absence of simplification +caused $\simp(\rup \backslash s)$ to +generate the nested alternatives structure: +\begin{center} +$ \oplus[\ZERO \;, \; _{bs}\oplus \textit{rs} ]$ +\end{center} +and this will always trigger the $\flatten$ to +spill out the inner alternative's bitcode $\textit{bs}$, +whereas when +simplification is done along the way, +the structure of nested alternatives is never created(we can +actually prove that simplification function never allows nested +alternatives to happen, more on this later). + +How about we do not allow the function $\simp$ +to fuse out the bits when it is unnecessary? +Like, for the above regular expression, we might +just delete the outer layer of alternative +\begin{center} +\st{$ {\oplus[\ZERO \;,}$} $_{bs}\oplus \textit{rs}$ \st{$]$} +\end{center} +and get $_{bs}\oplus \textit{rs}$ instead, without +fusing the bits $\textit{bs}$ inside to every element +of $\textit{rs}$. +This idea can be realized by making the following +changes to the $\simp$-function: +\begin{center} + \begin{tabular}{@{}lcl@{}} + + $\textit{simp}' \; (_{\textit{bs}}(a_1 \cdot a_2))$ & $\dn$ & $\textit{as} \; \simp \; \textit{was} \; \textit{before} $ \\ + + $\textit{simp}' \; (_{bs}\oplus as)$ & $\dn$ & \st{$\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $} \\ + &&\st{$\quad\textit{case} \; [] \Rightarrow \ZERO$} \\ + &&\st{$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$} \\ + &&\st{$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$}\\ + &&$\textit{if}(\textit{hollowAlternatives}( \textit{map \; simp \; as}))$\\ + &&$\textit{then} \; \fuse \; \textit{bs}\; \textit{extractAlt}(\textit{map} \; \simp \; \textit{as} )$\\ + &&$\textit{else} \; \simp(_{bs} \oplus \textit{as})$\\ + + + $\textit{simp}' \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ +\end{tabular} +\end{center} + +\noindent +given the definition of $\textit{hollowAlternatives}$ and $\textit{extractAlt}$ : +\begin{center} +$\textit{hollowAlternatives}( \textit{rs}) \dn +\exists r = (_{\textit{bs}_1}\oplus \textit{rs}_1) \in \textit{rs}. \forall r' \in \textit{rs}, \; +\textit{either} \; r' = \ZERO \; \textit{or} \; r' = r $ +$\textit{extractAlt}( \textit{rs}) \dn \textit{if}\big( +\exists r = (_{\textit{bs}_1}\oplus \textit{rs}_1) \in \textit{rs}. \forall r' \in \textit{rs}, \; +\textit{either} \; r' = \ZERO \; \textit{or} \; r' = r \big)\; \textit{then} \; \textit{return} \; r$ +\end{center} +\noindent +Basically, $\textit{hollowAlternatives}$ captures the feature of +a list of regular expression of the shape +\begin{center} +$ \oplus[\ZERO \;, \; _{bs}\oplus \textit{rs} ]$ +\end{center} +and this means we can simply elevate the +inner regular expression $_{bs}\oplus \textit{rs}$ + to the outmost +and throw away the useless $\ZERO$s and +the outer $\oplus$ wrapper. +Using this new definition of simp, +under the example where $r$ is the regular expression +$(a+b)(a+a*)$ and $s$ is the string $aa$ +the problem of $\rup\backslash_{simp} \, s \neq \simp(\rup\backslash s)$ +is resolved. + +Unfortunately this causes new problems: +for the counterexample where +\begin{center} +$r$ is the regular expression +$(ab+(a^*+aa))$ and $s$ is the string $aa$ +\end{center} + +\noindent +$\rup\backslash_{simp} \, s$ is equal to +$ _1(_{011}a^* + _1\ONE) $ whereas +$ \simp(\rup\backslash s) = (_{1011}a^* + _{11}\ONE)$. +This discrepancy does not appear for the old +version of $\simp$. + + +During the first derivative operation, +$\rup\backslash a=(_0\ONE + \ZERO)(_0a + _1a^*)$ is +in the form of a sequence regular expression with +two components, the first +one $\ONE + \ZERO$ being nullable. +Recall the simplification function definition: +\begin{center} + \begin{tabular}{@{}lcl@{}} + + $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ + &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ + &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ + &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\ + + $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ + &&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\ + &&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ + &&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\ + + $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ +\end{tabular} +\end{center} + +\noindent + +and the difinition of $\flatten$: + \begin{center} + \begin{tabular}{c c c} + $\flatten \; []$ & $\dn$ & $[]$\\ + $\flatten \; \ZERO::rs$ & $\dn$ & $rs$\\ + $\flatten \;(_{\textit{bs}_1}\oplus \textit{rs}_1 ::rs)$ & $\dn$ & $(\map \, (\fuse \, \textit{bs}_1) \,\textit{rs}_1) ::: \flatten(rs)$\\ + $\flatten \; r :: rs$ & $\dn$ & $r::\flatten(rs)$ + \end{tabular} + \end{center} + + \noindent + +If we call $\simp$ on $\rup\backslash a$, +then we would go throught the third clause of +the sequence case:$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$. +The $\ZERO$ of $(_0\ONE + \ZERO)$ is thrown away +by $\flatten$ and +$_0\ONE$ merged into $(_0a + _1a^*)$ by simply +putting its bits($_0$) to the front of the second component: + ${\bf_0}(_0a + _1a^*)$. + After a second derivative operation, + namely, $(_0(_0a + _1a^*))\backslash a$, we get + $ + _0(_0 \ONE + _1(_1\ONE \cdot a^*)) + $, and this simplifies to $_0(_0 \ONE + _{11} a^*)$ + by the third clause of the alternative case: + $\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$. +The outmost bit $_0$ stays with +the outmost regular expression, rather than being fused to +its child regular expressions, as what we will later see happens +to $\simp(\rup\backslash \, s)$. +If we choose to not simplify in the midst of derivative operations, +but only do it at the end after the string has been exhausted, +namely, $\simp(\rup\backslash \, s)=\simp((\rup\backslash a)\backslash a)$, +then at the {\bf second} derivative of +$(\rup\backslash a)\bf{\backslash a}$ +we will go throught the clause of $\backslash$: +\begin{center} +\begin{tabular}{lcl} +$(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ & + $(when \; \textit{bnullable}\,a_1)$\\ + & &$\textit{ALTS}\,bs\,List(\;\;(\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\ + & &$(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))\;\;)$\\ +\end{tabular} +\end{center} + +because +$\rup\backslash a = (_0\ONE + \ZERO)(_0a + _1a^*)$ +is a sequence +with the first component being nullable +(unsimplified, unlike the first round of running$\backslash_{simp}$). +Therefore $((_0\ONE + \ZERO)(_0a + _1a^*))\backslash a$ splits into +$([(\ZERO + \ZERO)\cdot(_0a + _1a^*)] + _0( _0\ONE + _1[_1\ONE \cdot a^*]))$. +After these two successive derivatives without simplification, +we apply $\simp$ to this regular expression, which goes through +the alternative clause, and each component of +$([(\ZERO + \ZERO)\cdot(_0a + _1a^*)] + _0( _0\ONE + _1[_1\ONE \cdot a^*]))$ +will be simplified, giving us the list:$[\ZERO, _0(_0\ONE + _{11}a^*)]$ +This list is then "flattened"--$\ZERO$ will be +thrown away by $\textit{flatten}$; $ _0(_0\ONE + _{11}a^*)$ +is opened up to make the list consisting of two separate elements +$_{00}\ONE$ and $_{011}a^*$, note that $flatten$ +$\fuse$s the bit(s) $_0$ to the front of $_0\ONE $ and $_{11}a^*$. +The order of simplification, which impacts the order that alternatives +are opened up, causes +the bits to be moved differently. + + + +We have changed the algorithm to suppress the old +counterexample, but this gives rise to new counterexamples. +This dilemma causes this amendment not a successful +attempt to make $\rup\backslash_{simp} \, s = \simp(\rup\backslash s)$ +under every possible regular expression and string. +\subsection{Properties of the Function $\simp$} + +We have proved in Isabelle quite a few properties +of the $\simp$-function, which helps the proof to go forward +and we list them here to aid comprehension. + +To start, we need a bit of auxiliary notations, +which is quite basic and is only written here +for clarity. + +$\textit{sub}(r)$ computes the set of the +sub-regular expression of $r$: +\begin{center} +$\textit{sub}(\ONE) \dn \{\ONE\}$\\ +$\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1 \cdot r_2\}$\\ +$\textit{sub}(r_1 + r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1+r_2\}$\\ +\end{center} +$\textit{good}(r) \dn r \neq \ZERO \land \\ +\forall r' \in \textit{sub}(r), \textit{if} \; r' = _{bs_1}\oplus(rs_1), \; +\textit{then} \nexists r'' \in \textit{rs}_1 \; s.t.\; +r'' = _{bs_2}\oplus \textit{rs}_2 $ + +The properties are mainly the ones below: +\begin{itemize} +\item +\begin{center} +$\simp(\simp(r)) = \simp(r)$ +\end{center} +\item +\begin{center} +$\textit{if} r = \simp(r') \textit{then} \; \textit{good}(r) $ +\end{center} +\end{itemize} +\subsection{the Contains relation} +$\retrieve$ is a too strong relation in that +it only extracts one bitcode instead of a set of them. +Therefore we try to define another relation(predicate) +to capture the fact the regular expression has bits +being moved around but still has all the bits needed. +The contains symbol, written$\gg$, is a relation that +takes two arguments in an infix form +and returns a truth value. + + +In other words, from the set of regular expression and +bitcode pairs +$\textit{RV} = \{(r, v) \mid r \text{r is a regular expression, v is a value}\}$, +those that satisfy the following requirements are in the set +$\textit{RV}_Contains$. +Unlike the $\retrieve$ +function, which takes two arguments $r$ and $v$ and +produces an only answer $\textit{bs}$, it takes only +one argument $r$ and returns a set of bitcodes that +can be generated by $r$. +\begin{center} +\begin{tabular}{llclll} +& & & $_{bs}\ONE$ & $\gg$ & $\textit{bs}$\\ +& & & $_{bs}{\bf c}$ & $\gg$ & $\textit{bs}$\\ +$\textit{if} \; r_1 \gg \textit{bs}_1$ & $r_2 \; \gg \textit{bs}_2$ +& $\textit{then}$ & + $_{bs}{r_1 \cdot r_2}$ & + $\gg$ & + $\textit{bs} @ \textit{bs}_1 @ \textit{bs}_2$\\ + + $\textit{if} \; r \gg \textit{bs}_1$ & & $\textit{then}$ & + $_{bs}{\oplus(r :: \textit{rs}})$ & + $\gg$ & + $\textit{bs} @ \textit{bs}_1 $\\ + + $\textit{if} \; _{bs}(\oplus \textit{rs}) \gg \textit{bs} @ \textit{bs}_1$ & & $\textit{then}$ & + $_{bs}{\oplus(r :: \textit{rs}})$ & + $\gg$ & + $\textit{bs} @ \textit{bs}_1 $\\ + + $\textit{if} \; r \gg \textit{bs}_1\; \textit{and}$ & $_{bs}r^* \gg \textit{bs} @ \textit{bs}_2$ & $\textit{then}$ & + $_{bs}r^* $ & + $\gg$ & + $\textit{bs} @ [0] @ \textit{bs}_1@ \textit{bs}_2 $\\ + + & & & $_{bs}r^*$ & $\gg$ & $\textit{bs} @ [1]$\\ +\end{tabular} +\end{center} +It is a predicate in the sense that given +a regular expression and a bitcode, it +returns true or false, depending on whether +or not the regular expression can actually produce that +value. If the predicates returns a true, then +we say that the regular expression $r$ contains +the bitcode $\textit{bs}$, written +$r \gg \textit{bs}$. +The $\gg$ operator with the +regular expression $r$ may also be seen as a +machine that does a derivative of regular expressions +on all strings simultaneously, taking +the bits by going throught the regular expression tree + structure in a depth first manner, regardless of whether + the part being traversed is nullable or not. + It put all possible bits that can be produced on such a traversal + into a set. + For example, if we are given the regular expression +$((a+b)(c+d))^*$, the tree structure may be written as +\begin{center} +\begin{tikzpicture} +\tikz[tree layout]\graph[nodes={draw, circle}] { +* -> + {@-> { + {+1 -> + {a , b} + }, + {+ -> + {c , d } + } + } + } +}; +\end{tikzpicture} +\end{center} +\subsection{the $\textit{ders}_2$ Function} +If we want to prove the result +\begin{center} + $ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$ +\end{center} +inductively +on the structure of the regular expression, +then we need to induct on the case $r_1 \cdot r_2$, +it can be good if we could express $(r_1 \cdot r_2) \backslash s$ +in terms of $r_1 \backslash s$ and $r_2 \backslash s$, +and this naturally induces the $ders2$ function, +which does a "convolution" on $r_1$ and $r_2$ using the string +$s$. +It is based on the observation that the derivative of $r_1 \cdot r_2$ +with respect to a string $s$ can actually be written in an "explicit form" +composed of $r_1$'s derivative of $s$ and $r_2$'s derivative of $s$. +This can be illustrated in the following procedure execution +\begin{center} + $ (r_1 \cdot r_2) \backslash [c_1c_2] = (\textit{if} \; \nullable(r_1)\; \textit{then} \; ((r_1 \backslash c_1) \cdot r_2 + r_2 \backslash c_1) \; \textit{else} \; (r_1\backslash c_1) \cdot r_2) \backslash c_2$ +\end{center} +which can also be written in a "convoluted sum" +format: +\begin{center} + $ (r_1 \cdot r_2) \backslash [c_1c_2] = \sum{r_1 \backslash s_i \cdot r_2 \backslash s_j}$ +\end{center} +In a more serious manner, we should write +\begin{center} + $ (r_1 \cdot r_2) \backslash [c_1c_2] = \sum{r_1 \backslash s_i \cdot r_2 \backslash s_j}$ +\end{center} +Note this differentiates from the previous form in the sense that +it calculates the results $r_1\backslash s_i , r_2 \backslash s_j$ first and then glue them together +through nested alternatives whereas the $r_1 \cdot r_2 \backslash s$ procedure, +used by algorithm $\lexer$, can only produce each component of the +resulting alternatives regular expression altogether rather than +generating each of the children nodes one by one +n a single recursive call that is only for generating that +very expression itself. +We have this +\section{Conclusion} +Under the exhaustive tests we believe the main +result holds, yet a proof still seems elusive. +We have tried out different approaches, and +found a lot of properties of the function $\simp$. +The counterexamples where $\rup\backslash_{simp} \, s \neq \simp(\rup\backslash s)$ +are also valuable in the sense that +we get to know better why they are not equal and what +are the subtle differences between a +nested simplified regular expression and a +regular expression that is simplified at the final moment. +We are almost there, but a last step is needed to make the proof work. +Hopefully in the next few weeks we will be able to find one. +%CONSTRUCTION SITE HERE +that is to say, despite the bits are being moved around on the regular expression +(difference in bits), the structure of the (unannotated)regular expression +after one simplification is exactly the same after the +same sequence of derivative operations +regardless of whether we did simplification +along the way. + One way would be to give a function that calls + +fuse is the culprit: it causes the order in which alternatives +are opened up to be remembered and finally the difference +appear in $\simp(\rup \backslash s)$ and $\rup \backslash{simp} \,s$. +but we have to use them as they are essential in the simplification: +flatten needs them. + + + +However, without erase the above equality does not hold: +for the regular expression +$(a+b)(a+a*)$, +if we do derivative with respect to string $aa$, +we get + +\subsection{Another Proof Strategy} +sdddddr does not equal sdsdsdsr sometimes.\\ +For example, + +This equicalence class method might still have the potential of proving this, +but not yet +i parallelly tried another method of using retrieve\\ + + +The vsimp function, defined as follows +tries to simplify the value in lockstep with +regular expression:\\ + + +The problem here is that + +we used retrieve for the key induction: +$decode (retrieve (r\backslash (s @ [c])) v) r $ +$decode (retrieve (r\backslash s) (inj (r\backslash s) c v)) r$ +Here, decode recovers a value that corresponds to a match(possibly partial) +from bits, and the bits are extracted by retrieve, +and the key value $v$ that guides retrieve is +$mkeps r\backslash s$, $inj r c (mkeps r\backslash s)$, $inj (inj (v))$, ...... +if we can +the problem is that +need vsiimp to make a value that is suitable for decoding +$Some(flex rid(s@[c])v) = Some(flex rids(inj (r\backslash s)cv))$ +another way that christian came up with that might circumvent the +prblem of finding suitable value is by not stating the visimp +function but include all possible value in a set that a regex is able to produce, +and proving that both r and sr are able to produce the bits that correspond the POSIX value + +produced by feeding the same initial regular expression $r$ and string $s$ to the + two functions $ders$ and $ders\_simp$. +The reason why +Namely, if $bmkeps( r_1) = bmkeps(r_2)$, then we + + +If we define the equivalence relation $\sim_{m\epsilon}$ between two regular expressions +$r_1$ and $r_2$as follows: +$r_1 \sim_{m\epsilon} r_2 \iff bmkeps(r_1)= bmkeps(r_2)$ +(in other words, they $r1$ and $r2$ produce the same output under the function $bmkeps$.) +Then the first goal +might be restated as +$(r^\uparrow)\backslash_{simp}\, s \sim_{m\epsilon} (r^\uparrow)\backslash s$. +I tried to establish an equivalence relation between the regular experssions +like dddr dddsr,..... +but right now i am only able to establish dsr and dr, using structural induction on r. +Those involve multiple derivative operations are harder to prove. +Two attempts have been made: +(1)induction on the number of der operations(or in other words, the length of the string s), +the inductive hypothesis was initially specified as +"For an arbitrary regular expression r, +For all string s in the language of r whose length do not exceed +the number n, ders s r me derssimp s r" +and the proof goal may be stated as +"For an arbitrary regular expression r, +For all string s in the language of r whose length do not exceed +the number n+1, ders s r me derssimp s r" +the problem here is that although we can easily break down +a string s of length n+1 into s1@list(c), it is not that easy +to use the i.h. as a stepping stone to prove anything because s1 may well be not +in the language L(r). This inhibits us from obtaining the fact that +ders s1 r me derssimps s1 r. +Further exploration is needed to amend this hypothesis so it includes the +situation when s1 is not nullable. +For example, what information(bits? +values?) can be extracted +from the regular expression ders(s1,r) so that we can compute or predict the possible +result of bmkeps after another derivative operation. What function f can used to +carry out the task? The possible way of exploration can be +more directly perceived throught the graph below: +find a function +f +such that +f(bders s1 r) += re1 +f(bderss s1 r) += re2 +bmkeps(bders s r) = g(re1,c) +bmkeps(bderssimp s r) = g(re2,c) +and g(re1,c) = g(re2,c) +The inductive hypothesis would be +"For all strings s1 of length <= n, +f(bders s1 r) += re1 +f(bderss s1 r) += re2" +proving this would be a lemma for the main proof: +the main proof would be +" +bmkeps(bders s r) = g(re1,c) +bmkeps(bderssimp s r) = g(re2,c) +for s = s1@c +" +and f need to be a recursive property for the lemma to be proved: +it needs to store not only the "after one char nullable info", +but also the "after two char nullable info", +and so on so that it is able to predict what f will compute after a derivative operation, +in other words, it needs to be "infinitely recursive"\\ +To prove the lemma, in other words, to get +"For all strings s1 of length <= n+1, +f(bders s1 r) += re3 +f(bderss s1 r) += re4"\\ +from\\ +"For all strings s1 of length <= n, +f(bders s1 r) += re1 +f(bderss s1 r) += re2"\\ +it might be best to construct an auxiliary function h such that\\ +h(re1, c) = re3\\ +h(re2, c) = re4\\ +and re3 = f(bder c (bders s1 r))\\ +re4 = f(simp(bder c (bderss s1 r))) +The key point here is that we are not satisfied with what bders s r will produce under +bmkeps, but also how it will perform after a derivative operation and then bmkeps, and two +derivative operations and so on. In essence, we are preserving the regular expression +itself under the function f, in a less compact way than the regluar expression: we are +not just recording but also interpreting what the regular expression matches. +In other words, we need to prove the properties of bderss s r beyond the bmkeps result, +i.e., not just the nullable ones, but also those containing remaining characters.\\ +(2)we observed the fact that +erase sdddddr= erase sdsdsdsr +that is to say, despite the bits are being moved around on the regular expression +(difference in bits), the structure of the (unannotated)regular expression +after one simplification is exactly the same after the +same sequence of derivative operations +regardless of whether we did simplification +along the way. +However, without erase the above equality does not hold: +for the regular expression +$(a+b)(a+a*)$, +if we do derivative with respect to string $aa$, +we get +%TODO +sdddddr does not equal sdsdsdsr sometimes.\\ +For example, + +This equicalence class method might still have the potential of proving this, +but not yet +i parallelly tried another method of using retrieve\\ + + + +\noindent\rule[0.5ex]{\linewidth}{1pt} + + + + + + +\bibliographystyle{plain} +\bibliography{root} + + +\end{document} +