% Chapter Template

%We also present the idempotency property proof

%of $\bsimp$, which leverages the idempotency proof of $\rsimp$.

%This reinforces our claim that the fixpoint construction

%originally required by Sulzmann and Lu can be removed in $\blexersimp$.

%Last but not least, we present our efforts and challenges we met

%in further improving the algorithm by data

%structures such as zippers.

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

%	SECTION strongsimp

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

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

\chapter{A Better Size Bound for Derivatives} % 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.

\lstset{style=myScalastyle}

This chapter is a ``work-in-progress''

chapter which records

extensions to our $\blexersimp$.

We make a conjecture that the finite

size bound from the previous chapter can be 

improved to a cubic bound.

We implemented our conjecture in Scala.

We intend to formalise this part in Isabelle/HOL at a

later stage.

%we have not been able to finish due to time constraints of the PhD.

Nevertheless, we outline the ideas we intend to use for the proof.

\section{A Stronger Version of Simplification}

We present further improvements

for our lexer algorithm $\blexersimp$.

We devise a stronger simplification algorithm,

called $\bsimpStrong$, which can prune away

similar components in two regular expressions at the same 

alternative level,

even if these regular expressions are not exactly the same.

We call the lexer that uses this stronger simplification function

$\blexerStrong$.

%Unfortunately we did not have time to 

%work out the proofs, like in

%the previous chapters.

We conjecture that both

\begin{center}

	$\blexerStrong \;r \; s = \blexer\; r\;s$

\end{center}

and 

\begin{center}

	$\llbracket \bdersStrong{a}{s} \rrbracket = O(\llbracket a \rrbracket^3)$

\end{center}

hold.

%but a formalisation

%is still future work.

We give an informal justification 

why the correctness and cubic size bound proofs

can be achieved

by exploring the connection between the internal

data structure of our $\blexerStrong$ and

Animirov's partial derivatives.

In our bitcoded lexing algorithm, (sub)terms represent (sub)matches.

For example, the regular expression 

\[

	aa \cdot a^*+ a \cdot a^* + aa\cdot a^*

\]

contains three terms, 

expressing three possibilities for how it can match some input.

The first and the third terms are identical, which means we can eliminate

the latter as it will not contribute to a POSIX value.

In $\bsimps$, the $\distinctBy$ function takes care of 

such instances.

The criteria $\distinctBy$ uses for removing a duplicate

$a_2$ in the list

\begin{center}

	$rs_a@[a_1]@rs_b@[a_2]@rs_c$

\end{center}

is that 

the two erased regular expressions are equal

\begin{center}

	$\rerase{a_1} = \rerase{a_2}$.

\end{center}

This is characterised as the $LD$ 

rewrite rule in figure \ref{rrewriteRules}.

The problem, however, is that identical components

in two slightly different regular expressions cannot be removed

by the $LD$ rule.

Consider the stronger simplification

\begin{equation}

	\label{eqn:partialDedup}

	(a+b+d) \cdot r_1 + (a+c+e) \cdot r_1 \stackrel{?}{\rightsquigarrow} (a+b+d) \cdot r_1 + (c+e) \cdot r_1

\end{equation}

where the $(\underline{a}+c+e)\cdot r_1$ is deleted in the right alternative

$a+c+e$.

This is permissible because we have $(a+\ldots)\cdot r_1$ in the left

alternative.

The difficulty is that such  ``buried''

alternatives-sequences are not easily recognised.

But simplification like this actually

cannot be omitted, if we want to have a better bound.

For example, the size of derivatives can still

blow up even with our $\textit{bsimp}$ 

function: 

consider again the example

$\protect((a^* + (aa)^* + \ldots + (\underbrace{a\ldots a}_{n a's})^* )^*)^*$,

and set $n$ to a relatively small number like $n=5$, then we get the following

exponential growth:

\begin{figure}[H]

\centering

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

\caption{Size of derivatives of $\blexersimp$ from chapter 5 for matching 

	$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$ 

	with strings 

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

\end{figure}

\noindent

One possible approach would be to apply the rewriting

rule

\[

	(a+b+d) \cdot r_1  \longrightarrow a \cdot r_1 + b \cdot r_1 + d \cdot r_1

\]

\noindent

which pushes the sequence into the alternatives

in our $\simp$ function.

This would then make the simplification shown in \eqref{eqn:partialDedup} possible.

Translating this rule into our $\textit{bsimp}$ function would simply

involve adding a new clause to the $\textit{bsimp}_{ASEQ}$ function:

\begin{center}

	\begin{tabular}{@{}lcl@{}}

		$\textit{bsimp}_{ASEQ} \; bs\; a \; b$ & $\dn$ & $ (a,\; b) \textit{match}$\\

						       && $\ldots$\\

   &&$\quad\textit{case} \; (_{bs1}\sum as, a_2') \Rightarrow _{bs1}\sum (

   \map \; (_{[]}\textit{ASEQ} \; \_ \; a_2') \; as)$\\

   &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow   _{bs}a_1' \cdot a_2'$ \\

	\end{tabular}

\end{center}

\noindent

Unfortunately,

if we introduce this clause in our

setting we would lose the POSIX property of our calculated values. 

For example given the regular expression 

\begin{center}

	$(a + ab)(bc + c)$

\end{center}

and the string $ab$,

then our algorithm generates the following

correct POSIX value

\begin{center}

	$\Seq \; (\Right \; ab) \; (\Right \; c)$.

\end{center}

Essentially it matches the string with the longer Right-alternative

in the first sequence (and

then the 'rest' with the character regular expression $c$ from the second sequence).

If we add the simplification above, however, 

then we would obtain the following value

\begin{center}

	$\Left \; (\Seq \; a \; (\Left \; bc))$

\end{center}

where the $\Left$-alternatives get priority. 

This violates the POSIX rules.

The reason for getting this undesired value

is that the new rule splits this regular expression up into 

a topmost alternative

\begin{center}

	$a\cdot(b c + c) + ab \cdot (bc + c)$,

\end{center}

which is a regular expression with a 

quite different meaning: the original regular expression

is a sequence, but the simplified regular expression is an alternative.

With an alternative the maximal munch rule no longer works.

A method to reconcile this problem is to do the 

transformation in \eqref{eqn:partialDedup} ``non-invasively'',

meaning that we traverse the list of regular expressions

%\begin{center}

%	$rs_a@[a]@rs_c$

%\end{center}

inside alternatives

\begin{center}

	$\sum ( rs_a@[a]@rs_c)$

\end{center}

using  a function similar to $\distinctBy$,

but this time 

we allow the following more general rewrite rule:

\begin{equation}

\label{eqn:cubicRule}

%\mbox{

%\begin{mathpar}	

	\inferrule * [Right = cubicRule]{\vspace{0mm} }{rs_a@[a]@rs_c 

			\stackrel{s}{\rightsquigarrow }

		rs_a@[\textit{prune} \; a \; rs_a]@rs_c }

%\end{mathpar}

%\caption{The rule capturing the pruning simplification needed to achieve

%a cubic bound}

\end{equation}

\noindent

%L \; a_1' = L \; a_1 \setminus (\cup_{a \in rs_a} L \; a)

where $\textit{prune} \;a \; acc$ traverses $a$

without altering the structure of $a$, but removing components in $a$

that have appeared in the accumulator $acc$.

For example

\begin{center}

	$\textit{prune} \;\;\; (r_a+r_f+r_g+r_h)r_d \;\; \; [(r_a+r_b+r_c)r_d, (r_e+r_f)r_d] $

\end{center}

should be equal to 

\begin{center}

	$(r_g+r_h)r_d$

\end{center}

because $r_gr_d$ and 

$r_hr_d$ are the only terms

that do not appeared in the accumulator list 

\begin{center}

$[(r_a+r_b+r_c)r_d, (r_e+r_f)r_d]$.

\end{center}

We implemented the

function $\textit{prune}$ in Scala (see figure \ref{fig:pruneFunc})

The function $\textit{prune}$ 

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

It does not just walk through a list looking for exact duplicates,

but prunes sub-expressions recursively.

It manages proper contexts by the helper functions

$\textit{removeSeqTail}$, $\textit{isOne}$ and $\textit{atMostEmpty}$.

\begin{figure}%[H]

\begin{lstlisting}[numbers=left]

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

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

      {

        //all components have been removed, meaning this is effectively a duplicate

        //flats will take care of removing this AZERO 

        case Nil => AZERO

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

        case rs1 => AALTS(bs, rs1)

      }

      case ASEQ(bs, r1, r2) => 

        //remove the r2 in (ra + rb)r2 to identify the duplicate contents of r1

        prune(r1, acc.map(r => removeSeqTail(r, erase(r2)))) match {

          //after pruning, returns 0

          case AZERO => AZERO

          //after pruning, got r1'.r2, where r1' is equal to 1

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

          //assemble the pruned head r1p with r2

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

        }

        //this does the duplicate component removal task

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

    }

\end{lstlisting}

\caption{The function $\textit{prune}$ is called recursively in the 

alternative case (line 2) and in the sequence case (line 12).

In the alternative case we keep all the accumulators the same, but

in the sequence case we are making necessary changes to the accumulators 

to allow correct de-duplication.}\label{fig:pruneFunc}

\end{figure}

\noindent

\begin{figure}

\begin{lstlisting}[numbers=left]

    def atMostEmpty(r: Rexp) : Boolean = r match {

      case ZERO => true

      case ONE => true

      case STAR(r) => atMostEmpty(r)

      case SEQ(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)

      case ALTS(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)

      case CHAR(_) => false

    }

    def isOne(r: Rexp) : Boolean = r match {

      case ONE => true

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

      case ALTS(r1, r2) => (isOne(r1) || isOne(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))

      case STAR(r0) => atMostEmpty(r0)

      case CHAR(c) => false

      case ZERO => false

    }

    def removeSeqTail(r: Rexp, tail: Rexp) : Rexp = 

      if (r == tail)

        ONE

      else {

        r match {

          case SEQ(r1, r2) => 

            if(r2 == tail) r1 else ZERO

          case r => ZERO

        }

      }

\end{lstlisting}

\end{figure}

\noindent

Suppose we feed 

\begin{center}

	$r= (\underline{\ONE}+(\underline{f}+b)\cdot g)\cdot (a\cdot(d\cdot e))$

\end{center}

and 

\begin{center}

	$acc = \{a\cdot(d\cdot e),f\cdot (g \cdot (a \cdot (d \cdot e))) \}$

\end{center}

as the input into $\textit{prune}$.

The end result will be

\[

	b\cdot(g\cdot(a\cdot(d\cdot e)))

\]

where the underlined components in $r$ are eliminated.

Looking more closely, at the topmost call 

\[

	\textit{prune} \quad (\ONE+

	(f+b)\cdot g)\cdot (a\cdot(d\cdot e)) \quad

	\{a\cdot(d\cdot e),f\cdot (g \cdot (a \cdot (d \cdot e))) \}

\]

The sequence clause will be called,

where a sub-call

\[

	\textit{prune} \;\; (\ONE+(f+b)\cdot g)\;\; \{\ONE, f\cdot g \}

\]

is made. The terms in the new accumulator $\{\ONE,\; f\cdot g \}$ come from

the two calls to $\textit{removeSeqTail}$:

\[

	\textit{removeSeqTail} \quad\;\; a \cdot(d\cdot e) \quad\;\; a \cdot(d\cdot e) 

\]

and

\[

	\textit{removeSeqTail} \quad \;\; 

	f\cdot(g\cdot (a \cdot(d\cdot e)))\quad  \;\; a \cdot(d\cdot e).

\]

The idea behind $\textit{removeSeqTail}$ is that

when pruning recursively, we need to ``zoom in''

to sub-expressions, and this ``zoom in'' needs to be performed

on the

accumulators as well, otherwise the deletion will not work.

The sub-call 

$\textit{prune} \;\; (\ONE+(f+b)\cdot g)\;\; \{\ONE, f\cdot g \}$

is simpler, which will trigger the alternative clause, causing

a pruning on each element in $(\ONE+(f+b)\cdot g)$,

leaving us with $b\cdot g$ only.

Our new lexer with stronger simplification

uses $\textit{prune}$ by making it 

the core component of the deduplicating function

called $\textit{distinctWith}$.

$\textit{DistinctWith}$ ensures that all verbose

parts of a regular expression are pruned away.

\begin{figure}[H]

\begin{lstlisting}[numbers=left]

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

      case SEQ(r1, r2)  => 

        turnIntoTerms(r1).flatMap(r11 => furtherSEQ(r11, r2))

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

          case ZERO => Nil

          case _ => r :: Nil

    }

    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

                )

            }

        }

\end{lstlisting}

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

\end{figure}

\noindent

Once a regular expression has been pruned,

all its components will be added to the accumulator

to remove any future regular expressions' duplicate components.

The function $\textit{bsimpStrong}$

is very much the same as $\textit{bsimp}$, just with

$\textit{distinctBy}$ replaced 

by $\textit{distinctWith}$.

\begin{figure}[H]

\begin{lstlisting}

    def bsimpStrong(r: ARexp): ARexp =

    {

      r match {

        case ASEQ(bs1, r1, r2) => (bsimpStrong(r1), bsimpStrong(r2)) match {

        case (AZERO, _) => AZERO

        case (_, AZERO) => AZERO

        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)

        case (r1s, AONE(bs2)) => fuse(bs1, r1s) //assert bs2 == Nil

        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)

        }

        case AALTS(bs1, rs) => {

          distinctWith(flats(rs.map(bsimpStrong(_))), prune) match {

            case Nil => AZERO

            case s :: Nil => fuse(bs1, s)

            case rs => AALTS(bs1, rs)

          }

        }

        case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)

        case r => r

      }

    }

    def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {

        case Nil => r

        case c::s => bdersStrong(s, bsimpStrong(bder(c, r)))

      }

\end{lstlisting}

\caption{The function

$\textit{bsimpStrong}$: a stronger version of $\textit{bsimp}$}

\end{figure}

\noindent

The benefits of using 

$\textit{prune}$ refining the finiteness bound

to a cubic bound has not been formalised yet.

Therefore we choose to use Scala code rather than an Isabelle-style formal 

definition like we did for $\simp$, as the definitions might change

to suit our proof needs.

In the rest of the chapter we will use this convention consistently.

%The function $\textit{prune}$ is used in $\distinctWith$.

%$\distinctWith$ is a stronger version of $\distinctBy$

%which not only removes duplicates as $\distinctBy$ would

%do, but also uses the $\textit{pruneFunction}$

%argument to prune away verbose components in a regular expression.\\

%\begin{figure}[H]

%\begin{lstlisting}

%   //a stronger version of simp

%    def bsimpStrong(r: ARexp): ARexp =

%    {

%      r match {

%        case ASEQ(bs1, r1, r2) => (bsimpStrong(r1), bsimpStrong(r2)) match {

%          //normal clauses same as simp

%        case (AZERO, _) => AZERO

%        case (_, AZERO) => AZERO

%        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)

%        //bs2 can be discarded

%        case (r1s, AONE(bs2)) => fuse(bs1, r1s) //assert bs2 == Nil

%        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)

%        }

%        case AALTS(bs1, rs) => {

%          //distinctBy(flat_res, erase)

%          distinctWith(flats(rs.map(bsimpStrong(_))), prune) match {

%            case Nil => AZERO

%            case s :: Nil => fuse(bs1, s)

%            case rs => AALTS(bs1, rs)

%          }

%        }

%        //stars that can be treated as 1

%        case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)

%        case r => r

%      }

%    }

%    def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {

%        case Nil => r

%        case c::s => bdersStrong(s, bsimpStrong(bder(c, r)))

%      }

%\end{lstlisting}

%\caption{The function $\bsimpStrong$ and $\bdersStrongs$}

%\end{figure}

%\noindent

%$\distinctWith$, is in turn used in $\bsimpStrong$:

%\begin{figure}[H]

%\begin{lstlisting}

%      //Conjecture: [| bdersStrong(s, r) |] = O([| r |]^3)