\documentclass[a4paper,UKenglish]{lipics}

\usepackage{graphic}

\usepackage{data}

\usepackage{tikz-cd}

%\usepackage{algorithm}

\usepackage{amsmath}

\usepackage[noend]{algpseudocode}

\usepackage{enumitem}

\usepackage{nccmath}

\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\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 size of regular expressions.

  We have tested the correctness of these extended rules, but have not 

  formally established their correctness. We also have not yet looked 

  at extended regular expressions, such as bounded repetitions,

  negation and back-references.

\end{abstract}

\section{Introduction}

While we believe derivatives of regular expressions is a beautiful 

concept (interms of ease to implementing them in functional programming

language and ease to reason about them formally), they have one major 

drawback: every derivative step can make regular expressions grow 

drastically in size. This in turn has negative effects on the runtime of 

the corresponding lexing algorithms. Consider for example the regular 

expression $(a+aa)^*$ and the short string $aaaaaaaaaaaa$. The size of

the corresponding derivative is already 8668 node assuming the derivatives

is seen as a tree. The reason for the poor runtime of the 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 depend on values being encoded as bitsequences.

(Vlue are the results of the lexing algorithms generate; they encode how

a regular expression matched a string.) We already know that the lexing 

algorithm \emph{without} simplification is correct. Therefore in the

past 6 months we were trying to prove  that the algorithm using bitsequences plus

our simplification rules is 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, because we already have a very good idea how to 

establish that our set our simplification rules keeps the size below a

relatively tight bound.

In order to prove the main theorem \eqref{mainthm}, we need to prove the

two functions produce the same output. The definition of these 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}

functions. Our main theorem \eqref{mainthm} therefore boils down to

proving the following two  propositions (depending on which branch the 

if-else clause takes). It establishes how the derivatives  \emph{with}

simplification do not change the computed result:

\begin{itemize}

\item{} 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{} 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 in Isabelle the second part. This is actually not 

too difficult because we can show that simplification does not change

the language of regular expressions. If we can prove the first case,

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 (computed result).

\begin{center}

$\blexer \; r^\uparrow  s = \lexer \;r \;s$

\end{center}

\noindent

\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

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

Using this feature of $\flex$  we can rewrite the lexing

$w.r.t \; s @ [c]$ in term of lexing 

$w.r.t \; s$:

\begin{center}

$\flex \; r \; id \; (s@[c]) \; v = \flex \;  r \; id \; s \; (inj \; (r\backslash s) \; c\; v)$.

\end{center}

\noindent

this allows us to use 

the inductive hypothesis to get

\begin{center} 

$ \flex \; r\; id\; (s@[c])\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$

\end{center}

\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.\\

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.

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$.

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 the first

part 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

If we call $\simp$ on $\rup$, 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 simplified away 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$ remains unchanged and stays with 

the outmost regular expression. However, things are a bit

different when it comes to $\simp(\rup\backslash \, s)$, because

without simplification,  first term of the sequence 

$\rup\backslash a=(_0\ONE  + \ZERO)(_0a  +  _1a^*)$ 

is not merged into the second component

and is nullable.

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--for

$([(\ZERO + \ZERO)\cdot(_0a  +  _1a^*)]$ it will be simplified into $\ZERO$

and then thrown away by $\textit{flatten}$; $ _0( _0\ONE  + _1[_1\ONE \cdot a^*]))$

 becomes  $ _{00}\ONE  + _{011}a^*]))$ because flatten opens up the alternative

 $\ONE + a^*$ and fuses the front bit(s) $_0$ to the front of $_0\ONE $ and $_{11}a^*$

 and get $_{00}$ and $_{011}$.

 %CONSTRUCTION SITE

and we can use this to construct a set of examples based 

on this type of behaviour of two operations:

$r_1$

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

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\\

%HERE CONSTRUCTION SITE

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