% 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 have not formalised this part in Isabelle/HOL. 
%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}

Let us first 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 more
input of the form $a \ldots a$.
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}
\caption{The helper functions of $\textit{prune}$: 
$\textit{atMostEmpty}$, $\textit{isOne}$ and $\textit{removeSeqTail}$. $\textit{atMostEmpty}
$ is a function that takes a regular expression and returns true only in case that it
contains nothing more than the empty string in its language. $\textit{isOne}$ tests whether
a regular expression is equivalent to $\ONE$. $\textit{removeSeqTail}$ is a function that
takes away the tail of a sequence regular expression.}
\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}$. This function allows ``partial de-duplication''
of a regular expression. When part of a regular expression has appeared before in the accumulator, we 
can remove that verbose component.}
\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 $\textit{bsimp}$, 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)
%      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
We conjecture that the above Scala function $\bdersStrongs$,
written $\bdersStrong{\_}{\_}$ as an infix notation, 
satisfies the following property:
\begin{conjecture}
	$\llbracket \bdersStrong{a}{s} \rrbracket = O(\llbracket a \rrbracket^3)$
\end{conjecture}
\noindent
The stronger version of $\blexersimp$'s
code in Scala looks like: 
\begin{figure}[H]
\begin{lstlisting}
      def strongBlexer(r: Rexp, s: String) : Option[Val] = {
        Try(Some(decode(r, strong_blex_simp(internalise(r), s.toList)))).getOrElse(None)
      }
      def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
        case Nil => {
          if (bnullable(r)) {
            mkepsBC(r)
          }
          else
            throw new Exception("Not matched")
        }
        case c::cs => {
          strong_blex_simp(strongBsimp(bder(c, r)), cs)
        }
      }
\end{lstlisting}
\end{figure}
\noindent
We call this lexer $\blexerStrong$.
This version is able to reduce the
size of the derivatives which 
otherwise 
triggered exponential behaviour in
$\blexersimp$.
Consider again the runtime for matching 
$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$ with strings 
of the form $\protect\underbrace{aa..a}_{n}$.
They produce the folloiwng graphs ($\blexerStrong$ on the left-hand-side and
$\blexersimp$ on the right-hand-side).
\begin{figure}[H]
\centering
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
\begin{tikzpicture}
\begin{axis}[
    %xlabel={$n$},
    myplotstyle,
    xlabel={input length},
    ylabel={size},
    width = 7cm,
    height = 5cm,
    ]
\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},
    width = 7cm,
    height = 5cm,
    ]
\addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};
\end{axis}
\end{tikzpicture}\\
\multicolumn{2}{l}{}
\end{tabular}    
\caption{}\label{fig:aaaaaStarStar}
\end{figure}
\noindent
We hope the correctness is preserved.
%We would like to preserve the correctness like the one 
%we had for $\blexersimp$:
The proof idea is to preserve the key lemma in chapter \ref{Bitcoded2}
such as in equation \eqref{eqn:cubicRule}.
\begin{conjecture}\label{cubicConjecture}
	$\blexerStrong \;r \; s = \blexer\; r\;s$
\end{conjecture}
\noindent
The idea is to maintain key lemmas in
chapter \ref{Bitcoded2} like
$r \stackrel{*}{\rightsquigarrow} \textit{bsimp} \; r$
with the new rewriting rule 
shown in figure \eqref{eqn:cubicRule} .

In the next sub-section,
we will describe why we 
believe a cubic size bound can be achieved with
the stronger simplification.
For this we give a short introduction to the
partial derivatives,
which were invented by Antimirov \cite{Antimirov95},
and then link them with the result of the function
$\bdersStrongs$.
 
\subsection{Antimirov's partial derivatives}
Partial derivatives were first introduced by 
Antimirov \cite{Antimirov95}.
They are very similar
to Brzozowski derivatives,
but split children of alternative regular expressions into 
multiple independent terms. This means the output of
partial derivatives is a 
set of regular expressions, defined as follows
\begin{center}  
	\begin{tabular}{lcl@{\hspace{-5mm}}l}
		$\partial_x \; (r_1 \cdot r_2)$ & 
		$\dn$ & $(\partial_x \; r_1) \cdot r_2 \cup
		\partial_x \; r_2 \;$ & $ \textit{if} \; \; \nullable\; r_1$\\
				      & & $(\partial_x \; r_1)\cdot r_2 \quad\quad$ & $ 
		      \textit{otherwise}$\\ 
		$\partial_x \; r^*$ & $\dn$ & $(\partial_x \; r) \cdot r^*$\\
		$\partial_x \; c $ & $\dn$ & $\textit{if} \; x = c \; 
		\textit{then} \;
		\{ \ONE\} \;\;\textit{else} \; \varnothing$\\
		$\partial_x(r_1+r_2)$ & $=$ & $\partial_x(r_1) \cup \partial_x(r_2)$\\
		$\partial_x(\ONE)$ & $=$ & $\varnothing$\\
		$\partial_x(\ZERO)$ & $\dn$ & $\varnothing$\\
	\end{tabular}
\end{center}
\noindent
The $\cdot$ in the example 
$(\partial_x \; r_1) \cdot r_2 $ 
is a shorthand notation for the cartesian product 
$(\partial_x \; r_1) \times \{ r_2\}$.
%Each element in the set generated by a partial derivative
%corresponds to a (potentially partial) match
%TODO: define derivatives w.r.t string s
Rather than joining the calculated derivatives $\partial_x r_1$ and $\partial_x r_2$ together
using the $\sum$ constructor, Antimirov put them into
a set.  This means many subterms will be de-duplicated
because they are sets.
For example, to compute what the derivative of the regular expression 
$x^*(xx + y)^*$
w.r.t. $x$ is, one can compute a partial derivative
and get two singleton sets $\{x^* \cdot (xx + y)^*\}$ and $\{x \cdot (xx + y) ^* \}$
from $\partial_x(x^*) \cdot (xx + y) ^*$ and $\partial_x((xx + y)^*)$.

The partial derivative w.r.t. a string is defined recursively:
\[
	\partial_{c::cs} r \dn \bigcup_{r'\in (\partial_c r)}
	\partial_{cs} r'
\]
Suppose an alphabet $\Sigma$, we use $\Sigma^*$ for the set of all possible strings
from the alphabet. 
The set of all possible partial derivatives is then defined
as the union of derivatives w.r.t all the strings: 
\begin{center}
	\begin{tabular}{lcl}
		$\textit{PDER}_{\Sigma^*} \; r $ & $\dn $ & $\bigcup_{w \in \Sigma^*}\partial_w \; r$
	\end{tabular}
\end{center}
\noindent
Consider now again our pathological case where we apply the more
aggressive 
simplification
\begin{center}
	$((a^* + (aa)^* + \ldots + (\underbrace{a\ldots a}_{n a's})^* )^*)^*$
\end{center}
let use abbreviate theis regular expression with $r$,
then we have that
\begin{center}
$\textit{PDER}_{\Sigma^*} \; r = 
\bigcup_{i=1}^{n}\bigcup_{j=0}^{i-1} \{ 
	(\underbrace{a \ldots a}_{\text{j a's}}\cdot
(\underbrace{a \ldots a}_{\text{i a's}})^*)\cdot r \}$, 
\end{center}
The union on the right-hand-side has $n * (n + 1) / 2$ terms.
This leads us to believe that the maximum number of terms needed
in our derivative is also only $n * (n + 1) / 2$.
Therefore
we conjecture that $\bsimpStrong$ is also able to achieve this
upper limit in general.
\begin{conjecture}\label{bsimpStrongInclusionPder}
	Using a suitable transformation $f$, we have that
	\begin{center}
		$\forall s.\; f \; (r \bdersStrong  \; s) \subseteq
		 \textit{PDER}_{\Sigma^*} \; r$
	\end{center}
	holds.
\end{conjecture}
\noindent
The reason is that our \eqref{eqn:cubicRule} will keep only one copy of each term,
where the function $\textit{prune}$ takes care of maintaining
a set like structure similar to partial derivatives.
%We might need to adjust $\textit{prune}$
%slightly to make sure all duplicate terms are eliminated,
%which should be doable.

Antimirov had proven that the sum of all the partial derivative 
terms' sizes is bounded by the cubic of the size of that regular
expression:
\begin{property}\label{pderBound}
	$\llbracket \textit{PDER}_{\Sigma^*} \; r \rrbracket \leq O(\llbracket r \rrbracket^3)$
\end{property}
\noindent
This property was formalised by Wu et al. \cite{Wu2014}, and the 
details can be found in the Archive of Formal Froofs\footnote{https://www.isa-afp.org/entries/Myhill-Nerode.html}.
Once conjecture \ref{bsimpStrongInclusionPder} is proven, then property \ref{pderBound}
would provide us with a cubic bound for our $\blexerStrong$ algorithm: 
\begin{conjecture}\label{strongCubic}
	$\llbracket r \bdersStrong\; s \rrbracket \leq \llbracket r \rrbracket^3$
\end{conjecture}
\noindent
We leave this as future work.


%To get all the "atomic" components of a regular expression's possible derivatives,
%there is a procedure Antimirov called $\textit{lf}$, short for "linear forms", that takes
%whatever character is available at the head of the string inside the language of a
%regular expression, and gives back the character and the derivative regular expression
%as a pair (which he called "monomial"):
% \begin{center}  
% \begin{tabular}{ccc}
% $\lf(\ONE)$ & $=$ & $\phi$\\
%$\lf(c)$ & $=$ & $\{(c, \ONE) \}$\\
% $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
% $\lf(r^*)$ & $=$ & $\lf(r) \bigodot \lf(r^*)$\\
%\end{tabular}
%\end{center}
%%TODO: completion
%
%There is a slight difference in the last three clauses compared
%with $\partial$: instead of a dot operator $ \textit{rset} \cdot r$ that attaches the regular 
%expression $r$ with every element inside $\textit{rset}$ to create a set of 
%sequence derivatives, it uses the "circle dot" operator $\bigodot$ which operates 
%on a set of monomials (which Antimirov called "linear form") and a regular 
%expression, and returns a linear form:
% \begin{center}  
% \begin{tabular}{ccc}
% $l \bigodot (\ZERO)$ & $=$ & $\phi$\\
% $l \bigodot (\ONE)$ & $=$ & $l$\\
% $\phi \bigodot t$ & $=$ & $\phi$\\
% $\{ (x, \ZERO) \} \bigodot t$ & $=$ & $\{(x,\ZERO) \}$\\
% $\{ (x, \ONE) \} \bigodot t$ & $=$ & $\{(x,t) \}$\\
%  $\{ (x, p) \} \bigodot t$ & $=$ & $\{(x,p\cdot t) \}$\\
% $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
% $\lf(r^*)$ & $=$ & $\lf(r) \cdot \lf(r^*)$\\
%\end{tabular}
%\end{center}
%%TODO: completion
%
% Some degree of simplification is applied when doing $\bigodot$, for example,
% $l \bigodot (\ZERO) = \phi$ corresponds to $r \cdot \ZERO \rightsquigarrow \ZERO$,
% and  $l \bigodot (\ONE) = l$ to $l \cdot \ONE \rightsquigarrow l$, and
%  $\{ (x, \ZERO) \} \bigodot t = \{(x,\ZERO) \}$ to $\ZERO \cdot x \rightsquigarrow \ZERO$,
%  and so on.
%  
%  With the function $\lf$ one can compute all possible partial derivatives $\partial_{UNIV}(r)$ of a regular expression $r$ with 
%  an iterative procedure:
%   \begin{center}  
% \begin{tabular}{llll}
%$\textit{while}$ & $(\Delta_i \neq \phi)$  &                &          \\
% 		       &  $\Delta_{i+1}$           &        $ =$ & $\lf(\Delta_i) - \PD_i$ \\
%		       &  $\PD_{i+1}$              &         $ =$ & $\Delta_{i+1} \cup \PD_i$ \\
%$\partial_{UNIV}(r)$ & $=$ & $\PD$ &		     
%\end{tabular}
%\end{center}
%
%
% $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$,




%----------------------------------------------------------------------------------------
%	SECTION 2
%----------------------------------------------------------------------------------------


%The closed form for them looks like:
%%\begin{center}
%%	\begin{tabular}{llrclll}
%%		$r^{\{n+1\}}$ & $ \backslash_{rsimps}$ & $(c::s)$ & $=$ & & \\
%%		$\textit{rsimp}$ & $($ & $
%%		\sum \; ( $ & $\map$ & $(\textit{optermsimp}\;r)$ & $($\\
%%			 & & & & $\textit{nupdates} \;$ & 
%%			 $ s \; r_0 \; [ \textit{Some} \; ([c], n)]$\\
%%			 & & & & $)$ &\\
%%			 & &  $)$ & & &\\
%%			 & $)$ & & & &\\
%%	\end{tabular}
%%\end{center}
%\begin{center}
%	\begin{tabular}{llrcllrllll}
%		$r^{\{n+1\}}$ & $ \backslash_{rsimps}$ & $(c::s)$ & $=$ & & &&&&\\
%			      &&&&$\textit{rsimp}$ & $($ & $
%			      \sum \; ( $ & $\map$ & $(\textit{optermsimp}\;r)$ & $($\\
%					  &&&& & & & & $\;\; \textit{nupdates} \;$ & 
%			 		  $ s \; r_0 \; [ \textit{Some} \; ([c], n)]$\\
%					  &&&& & & & & $)$ &\\
%					  &&&& & &  $)$ & & &\\
%					  &&&& & $)$ & & & &\\
%	\end{tabular}
%\end{center}
%The $\textit{optermsimp}$ function with the argument $r$ 
%chooses from two options: $\ZERO$ or 
%We define for the $r^{\{n\}}$ constructor something similar to $\starupdate$
%and $\starupdates$:
%\begin{center}
%	\begin{tabular}{lcl}
%		$\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
%		$\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
%						     & & $\textit{if} \; 
%						     (\rnullable \; (\rders \; r \; s))$ \\
%						     & & $\textit{then} \;\; (s @ [c]) :: [c] :: (
%						     \starupdate \; c \; r \; Ss)$ \\
%						     & & $\textit{else} \;\; (s @ [c]) :: (
%						     \starupdate \; c \; r \; Ss)$
%	\end{tabular}
%\end{center}
%\noindent
%As a generalisation from characters to strings,
%$\starupdates$ takes a string instead of a character
%as the first input argument, and is otherwise the same
%as $\starupdate$.
%\begin{center}
%	\begin{tabular}{lcl}
%		$\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
%		$\starupdates \; (c :: cs) \; r \; Ss$ &  $=$ &  $\starupdates \; cs \; r \; (
%		\starupdate \; c \; r \; Ss)$
%	\end{tabular}
%\end{center}
%\noindent



%\section{Zippers}
%Zipper is a data structure designed to operate on 
%and navigate between local parts of a tree.
%It was first formally described by Huet \cite{HuetZipper}.
%Typical applications of zippers involve text editor buffers
%and proof system databases.
%In our setting, the idea is to compactify the representation
%of derivatives with zippers, thereby making our algorithm faster.
%Some initial results 
%We first give a brief introduction to what zippers are,
%and other works
%that apply zippers to derivatives
%When dealing with large trees, it would be a waste to 
%traverse the entire tree if
%the operation only
%involves a small fraction of it.
%The idea is to put the focus on that subtree, turning other parts
%of the tree into a context
%
%
%One observation about our derivative-based lexing algorithm is that
%the derivative operation sometimes traverses the entire regular expression
%unnecessarily:


%----------------------------------------------------------------------------------------
%	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$ regular expression
% is creating a value for it.
% For other regular expressions, the value aligns with the 
% structure of the regular expression:
% \[
% \vdash \Seq(\Char(a), \Char(b)) : a \cdot b
% \]
%But for the $~r$ regular expression, $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 regular expression, 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 regular expression 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})
% \]
% 
%
%\begin{center}
%	\begin{tabular}{lcl}
%		$\ntset \; r \; (n+1) \; c::cs $ & $\dn$ & $\nupdates \;
%		cs \; r \; [\Some \; ([c], n)]$\\
%		$\ntset \; r\; 0 \; \_$ &  $\dn$ &  $\None$\\
%		$\ntset \; r \; \_ \; [] $ & $ \dn$ & $[]$\\
%	\end{tabular}
%\end{center}

