% Chapter Template

\chapter{A Better Bound and Other Extensions} % Main chapter title

\label{Cubic} %In Chapter 5\ref{Chapter5} we discuss stronger simplifications to improve the finite bound

%in Chapter 4 to a polynomial one, and demonstrate how one can extend the

%algorithm to include constructs such as bounded repetitions and negations.

%----------------------------------------------------------------------------------------

%	SECTION strongsimp

%----------------------------------------------------------------------------------------

\section{A Stronger Version of Simplification}

%TODO: search for isabelle proofs of algorithms that check equivalence 

It will either match 2 $a$'s, then 0 or more $a$'s, in other words, at least 2 more $a$'s

\begin{figure}\label{string_3parts1}

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=3]

        {Consumed Input

        \nodepart{two} Expects $aa$

         \nodepart{three} Then expects $a^*$};

\end{tikzpicture}

\end{center}

\end{figure}

\noindent

Or it will match at least 1 more $a$:

\begin{figure}\label{string_3parts2}

\begin{center}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=3]

        {Consumed

        \nodepart{two} Expects $a$

         \nodepart{three} Then expects $a^*$};

\end{tikzpicture}

\end{center}

\end{figure}

If these two possibilities are identical, we can eliminate

the second one as we know the second one corresponds to 

a match that is not $\POSIX$.

If two identical regexes 

happen to be grouped into different sequences, one cannot use

the $a + a \rightsquigarrow a$ rule to eliminate them, even if they 

are "parallel" to each other:

\[

(a+b) \cdot r_1 + (a+c) \cdot r_2 \rightsquigarrow (a+b) \cdot r_1 + (c) \cdot r_2

\]

and that's because they are followed by possibly 

different "suffixes" $r_1$ and $r_2$, and if 

they do turn out to be different then doing 

\[

(a+b) \cdot r_1 + (a+c) \cdot r_2 \rightsquigarrow (a+b) \cdot r_1 + (c) \cdot r_2

\]

might cause a possible match where the string is in $L(a \cdot r_2)$ to be lost.

Here is an example for this.

Assume we have the derivative regex 

\[( r_1  +  r_2  +  r_3)\cdot r+ 

( r_1  +  r_5  +  r_6)\cdot( r_1  +  r_2  +  r_3)^*

\]

occurring in an intermediate step in our bit-coded lexing algorithm.

In this expression, there will be 6 "parallel" terms if we break up regexes 

of shape $(a+b)\cdot c$ using the distributivity law (into $ac + bc$).

\begin{align}

(\nonumber \\

 r_1  + &    \label{term:1} \\

 r_2  + &  \label{term:2} \\

 r_3 &  \label{term:3} \\

&	)\cdot r\; + \; (\nonumber \\

 r_1  + & \label{term:4} \\

 r_5  + & \label{term:5} \\

 r_6 \label{term:6}\\

&      )\cdot r\nonumber

\end{align}

They have been labelled, and each label denotes  

one term, for example, \ref{term:1} denotes

\[

 r_1 \cdot r

\]

\noindent

and \ref{term:3} denotes

\[

 r_3\cdot r.

\]

From a lexer's point of view, \ref{term:4} will never 

be picked up in later phases of matching because there

is a term \ref{term:1} giving identical matching information.

The first term \ref{term:1} will match a string in $L(r_1 \cdot  r)$, 

and so on for term \ref{term:2}, \ref{term:3}, etc.

\mybox{previous input $\ldots$}\mybox{$aaa$ }\mybox{rest of input $\ldots$}

\begin{center}\label{string_2parts}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2]

        {$r_{x1}$

         \nodepart{two} $r_1\cdot r$ };

%\caption{term 1 \ref{term:1}'s matching configuration}

\end{tikzpicture}

\end{center}

For term 1 \ref{term:1}, whatever was before the current

input position was fully matched and the regex corresponding

to it reduced to $\ONE$, 

and in the next input token, it will start on $r_1\cdot r$.

The resulting value will be something of a similar configuration:

\begin{center}\label{value_2parts}

%\caption{term 1 \ref{term:1}'s matching configuration}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2]

        {$v_{x1}$

         \nodepart{two} $v_{r_1\cdot r}$ };

\end{tikzpicture}

\end{center}

For term 2 \ref{term:2} we have a similar value partition:

\begin{center}\label{value_2parts2}

%\caption{term 1 \ref{term:1}'s matching configuration}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2]

        {$v_{x2}$

         \nodepart{two} $v_{r_2\cdot r}$ };

\end{tikzpicture}

\end{center}

\noindent

and so on.

We note that for term 4 \ref{term:4} its result value 

after any position beyond  the current one will always

be the same:

\begin{center}\label{value_2parts4}

%\caption{term 1 \ref{term:1}'s matching configuration}

\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]

    \node [rectangle split, rectangle split horizontal, rectangle split parts=2]

        {$v_{x4}$

         \nodepart{two} $v_{r_1\cdot r}$ };

\end{tikzpicture}

\end{center}

And $\POSIX$ rules says that we can eliminate at least one of them.

Our algorithm always puts the regex with the longest initial sub-match at the left of the 

alternatives, so we safely throw away \ref{term:4}.

The fact that term 1 and 4 are not immediately in the same alternative

expression does not prevent them from being two duplicate matches at

the current point of view.

To implement this idea into an algorithm, we define a "pruning function"

$\textit{prune}$, that takes away parts of all terms in $r$ that belongs to

$\textit{acc}$, which acts as an element

is a stronger version of $\textit{distinctBy}$.

Here is a concise version of it (in the style of Scala):

def distinctByPlus(rs: List[ARexp], acc: Set[Rexp] = Set()) : 

List[ARexp] =  rs match {

  case Nil => Nil

  case r :: rs =>

    if(acc.contains(erase(r)))

      distinctByPlus(rs, acc)

    else 

      prune(r, acc) :: distinctByPlus(rs, prune(r, acc) +: acc)

}

But for the function $\textit{prune}$ there is a difficulty:

how could one define the $L$ function in a "computable" way,

so that they generate a (lazy infinite) set of strings in $L(r)$.

We also need a function that tests whether $L(r_1) \subseteq L(r_2)$

is true.

For the moment we cut corners and do not define these two functions

as they are not used by Antimirov (and will probably not contribute

to a bound better than Antimirov's cubic bound).

Rather, we do not try to eliminate in every instance of regular expressions

that have "language duplicates", but only eliminate the "exact duplicates".

For this we need to break up terms $(a+b)\cdot c$ into two

terms $a\cdot c$ and $b\cdot c$ before we add them to the accumulator:

def distinctWith(rs: List[ARexp], 

                pruneFunction: (ARexp, Set[Rexp]) => ARexp, 

                acc: Set[Rexp] = Set()) : List[ARexp] = 

  rs match{

    case Nil => Nil

    case r :: rs => 

      if(acc(erase(r)))

        distinctWith(rs, pruneFunction, acc)

      else {

        val pruned_r = pruneFunction(r, acc)

        pruned_r :: 

        distinctWith(rs, 

          pruneFunction, 

          turnIntoTerms(erase(pruned_r)) ++: acc

        )

      }

  }

\caption{A Stronger Version of $\textit{distinctBy}$}

\end{figure}

\noindent

This process is done by the function $\textit{turnIntoTerms}$:

\begin{figure}

\begin{verbatim}

def turnIntoTerms(r: Rexp): List[Rexp] = r match {

  case SEQ(r1, r2)  => if(isOne(r1)) 

                          turnIntoTerms(r2) 

                       else 

                          turnIntoTerms(r1).map(r11 => SEQ(r11, r2))

  case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)

  case ZERO => Nil

  case _ => r :: Nil

}

\end{verbatim}

\caption{function that breaks up regular expression into "atomic" terms}

\end{figure}

\noindent

The pruning function can be defined recursively:

\begin{figure}

\begin{verbatim}

def prune7(r: ARexp, acc: Set[Rexp]) : ARexp = r match{

  case AALTS(bs, rs) => rs.map(r => prune7(r, acc)).filter(_ != ZERO) match

  {

    case Nil => AZERO

    case r::Nil => fuse(bs, r)

    case rs1 => AALTS(bs, rs1)

  }

  case ASEQ(bs, r1, r2) => prune7(r1, acc.map(r => removeSeqTail(r, erase(r2)))) match {

    case AZERO => AZERO

    case r1p if(isOne(erase(r1p))) => fuse(bs ++ mkepsBC(r1p), r2)

    case r1p => ASEQ(bs, r1p, r2)

  }

  case r => if(acc(erase(r))) AZERO else r

}

\end{verbatim}

\caption{pruning function}

\end{figure}

\begin{figure}

\centering

\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}

\begin{tikzpicture}

\begin{axis}[

    %xlabel={$n$},

    myplotstyle,

    xlabel={input length},

    ylabel={size},

    ]

\addplot[red,mark=*, mark options={fill=white}] table {strongSimpCurve.data};

\end{axis}

\end{tikzpicture}

  &

\begin{tikzpicture}

\begin{axis}[

    %xlabel={$n$},

    myplotstyle,

    xlabel={input length},

    ylabel={size},

    ]

\addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};

\end{axis}

\end{tikzpicture}\\

\multicolumn{2}{l}{Graphs: Runtime for matching $((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$ with strings 

           of the form $\underbrace{aa..a}_{n}$.}

\end{tabular}    

\caption{aaaaaStarStar} \label{fig:aaaaaStarStar}

\end{figure}

%----------------------------------------------------------------------------------------

%	SECTION 1

%----------------------------------------------------------------------------------------

\section{Adding Support for the Negation Construct, and its Correctness Proof}

We now add support for the negation regular expression:

\[			r ::=   \ZERO \mid  \ONE

			 \mid  c  

			 \mid  r_1 \cdot r_2

			 \mid  r_1 + r_2   

			 \mid r^*    

			 \mid \sim r

\]

The $\textit{nullable}$ function's clause for it would be 

\[

\textit{nullable}(~r) = \neg \nullable(r)

\]

The derivative would be

\[

~r \backslash c = ~ (r \backslash c)

\]

The most tricky part of lexing for the $~r$ regex

 is creating a value for it.

 For other regular expressions, the value aligns with the 

 structure of the regex:

 \[

 \vdash \Seq(\Char(a), \Char(b)) : a \cdot b

 \]

But for the $~r$ regex, $s$ is a member of it if and only if

$s$ does not belong to $L(r)$. 

That means when there

is a match for the not regex, it is not possible to generate how the string $s$ matched

with $r$. 

What we can do is preserve the information of how $s$ was not matched by $r$,

and there are a number of options to do this.

We could give a partial value when there is a partial match for the regex inside

the $\mathbf{not}$ construct.

For example, the string $ab$ is not in the language of $(a\cdot b) \cdot c$,

A value for it could be 

 \[

 \vdash \textit{Not}(\Seq(\Char(a), \Char(b))) : ~((a \cdot b ) \cdot c)

 \]

 The above example demonstrates what value to construct 

 when the string $s$ is at most a real prefix

 of the strings in $L(r)$. When $s$ instead is not a prefix of any strings

 in $L(r)$, it becomes unclear what to return as a value inside the $\textit{Not}$

 constructor.

 Another option would be to either store the string $s$ that resulted in 

 a mis-match for $r$ or a dummy value as a placeholder:

 \[

 \vdash \textit{Not}(abcd) : ~( r_1 )

 \]

or

 \[

 \vdash \textit{Not}(\textit{Dummy}) : ~( r_1 )

 \] 

 We choose to implement this as it is most straightforward:

 \[

 \mkeps(~(r))  = \textit{if}(\nullable(r)) \; \textit{Error} \; \textit{else} \; \textit{Not}(\textit{Dummy})

 \]

%----------------------------------------------------------------------------------------

%	SECTION 2

%----------------------------------------------------------------------------------------

\section{Bounded Repetitions}