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

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

The correctness proof of

\begin{center}

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

\end{center}

\noindent

might provide us insight into proving 

\begin{center}

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

\end{center}

\noindent

(that is also

why we say the new proof builds on the older one).

The proof defined the function $\flex$ as another way of

expressing the $\lexer$ function:

\begin{center}

$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; r\backslash s)$

\end{center}.

\noindent

(proof for the above equality will be explained later)

The definition of $flex$ is as follows:

\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

here $\flex$ 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

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

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

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

\end{center}

\noindent

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

%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

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: