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

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

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

\begin{center}

$\rup\backslash_{simp} \, s$ is equal to $_0(_0\ONE +_{11}a^*)$

\end{center}

\noindent

whereas

\begin{center}

\end{center}

\noindent

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 

property: one simplification in the end causes the 

same regular expression structure as

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$

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

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