% 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.
\lstset{style=myScalastyle}
This chapter is a ``miscellaneous''
chapter which records various
extensions to our $\blexersimp$'s formalisations.\\
Firstly we present further improvements
made to 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$.
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 formalising
them is still work in progress.
We give reasons 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.\\
Secondly, we extend our $\blexersimp$
to support bounded repetitions ($r^{\{n\}}$).
We update our formalisation of
the correctness and finiteness properties to
include this new construct. With bounded repetitions
we are able to out-compete other verified lexers such as
Verbatim++ on regular expressions which involve a lot of
repetitions. %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
%----------------------------------------------------------------------------------------
\section{A Stronger Version of Simplification}
%TODO: search for isabelle proofs of algorithms that check equivalence
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 it will match future input.
The first and the third terms are identical, which means we can eliminate
the latter as we know it will not be picked up by $\bmkeps$.
In $\bsimps$, the $\distinctBy$ function takes care of this.
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
\begin{center}
$\rerase{a_1} = \rerase{a_2}$.
\end{center}
It can be characterised as the $LD$
rewrite rule in \ref{rrewriteRules}.\\
The problem , however, is that identical components
in two slightly different regular expressions cannot be removed:
\begin{figure}[H]
\[
(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
\]
\caption{Desired simplification, but not done in $\blexersimp$}\label{partialDedup}
\end{figure}
\noindent
A simplification like this actually
cannot be omitted,
as without it the size could blow up even with our $\simp$ function:
\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{Runtime of $\blexersimp$ for matching
$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$
with strings
of the form $\protect\underbrace{aa..a}_{n}$.}\label{blexerExp}
\end{figure}
\noindent
We would like to apply the rewriting at some stage
\begin{figure}[H]
\[
(a+b+d) \cdot r_1 \longrightarrow a \cdot r_1 + b \cdot r_1 + d \cdot r_1
\]
\caption{Desired simplification, but not done in $\blexersimp$}\label{desiredSimp}
\end{figure}
\noindent
in our $\simp$ function,
so that it makes the simplification in \ref{partialDedup} possible.
For example,
can a function like the below one be used?
%TODO: simp' that spills things
Unfortunately,
if we introduce them 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
\begin{center}
$ab$,
\end{center}
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, then we obtain the following value
\begin{center}
$\Left \; (\Seq \; a \; (\Left \; bc))$
\end{center}
where the $\Left$-alternatives get priority.
However this violates the POSIX rules.
The reason for getting this undesired value
is that the new rule splits this regular expression up into
\begin{center}
$a\cdot(b c + c) + ab \cdot (bc + c)$,
\end{center}
which becomes a regular expression with a
totally different structure--the original
was a sequence, and now it becomes an alternative.
With an alternative the maximum munch rule no longer works.\\
A method to reconcile this is to do the
transformation in \ref{desiredSimp} ``non-invasively'',
meaning that we traverse the list of regular expressions
\begin{center}
$rs_a@[a]@rs_c$
\end{center}
in the alternative
\begin{center}
$\sum ( rs_a@[a]@rs_c)$
\end{center}
using a function similar to $\distinctBy$,
but this time
we allow a more general list rewrite:
\begin{mathpar}\label{cubicRule}
\inferrule{\vspace{0mm} }{rs_a@[a]@rs_c
\stackrel{s}{\rightsquigarrow }
rs_a@[\textit{prune} \; a \; rs_a]@rs_c }
\end{mathpar}
%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$, 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 have 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
function $\textit{prune}$ in Scala,
and incorporated into our lexer,
by replacing the $\simp$ function
with a stronger version called $\bsimpStrong$
that prunes regular expressions.
We call this lexer $\blexerStrong$.
$\blexerStrong$ is able to drastically reduce the
internal data structure size which could
trigger exponential behaviours in
$\blexersimp$.
\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},
]
\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}
\begin{figure}[H]
\begin{lstlisting}
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))//rs.forall(atMostEmpty) && rs.exists(isOne)
case STAR(r0) => atMostEmpty(r0)
case CHAR(c) => false
case ZERO => false
}
//r = r' ~ tail' : If tail' matches tail => returns r'
def removeSeqTail(r: Rexp, tail: Rexp) : Rexp = r match {
case SEQ(r1, r2) =>
if(r2 == tail)
r1
else
ZERO
case r => ZERO
}
def prune(r: ARexp, acc: Set[Rexp]) : ARexp = r match{
case AALTS(bs, rs) => rs.map(r => prune(r, acc)).filter(_ != ZERO) 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{pruning function together with its helper functions}
\end{figure}
\noindent
The benefits of using
$\textit{prune}$ such as 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 proof needs.
In the rest of the chapter we will use this convention consistently.
\begin{figure}[H]
\begin{lstlisting}
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}$}
\end{figure}
\noindent
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
}
}
\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}
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 would like to preserve the correctness like the one
we had for $\blexersimp$:
\begin{conjecture}\label{cubicConjecture}
$\blexerStrong \;r \; s = \blexer\; r\;s$
\end{conjecture}
\noindent
We introduce the new rule \ref{cubicRule}
and augment our proofs in chapter \ref{Bitcoded2}.
The idea is to maintain the properties like
$r \stackrel{*}{\rightsquigarrow} \textit{bsimp} \; r$ etc.
In the next section,
we will describe why we
believe a cubic bound can be achieved.
We give an introduction to the
partial derivatives,
which was invented by Antimirov \cite{Antimirov95},
and then link it with the result of the function
$\bdersStrongs$.
\section{Antimirov's partial derivatives}
This suggests a link towrads "partial derivatives"
introduced The idea behind Antimirov's partial derivatives
is to do derivatives in a similar way as suggested by Brzozowski,
but maintain a set of regular expressions instead of a single one:
%TODO: antimirov proposition 3.1, needs completion
\begin{center}
\begin{tabular}{ccc}
$\partial_x(a+b)$ & $=$ & $\partial_x(a) \cup \partial_x(b)$\\
$\partial_x(\ONE)$ & $=$ & $\phi$
\end{tabular}
\end{center}
Rather than joining the calculated derivatives $\partial_x a$ and $\partial_x b$ together
using the alternatives constructor, Antimirov cleverly chose to put them into
a set instead. This breaks the terms in a derivative regular expression up,
allowing us to understand what are the "atomic" components of it.
For example, To compute what regular expression $x^*(xx + y)^*$'s
derivative against $x$ is made of, one can do a partial derivative
of it 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)^*)$.
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
%----------------------------------------------------------------------------------------
\section{Bounded Repetitions}
We have promised in chapter \ref{Introduction}
that our lexing algorithm can potentially be extended
to handle bounded repetitions
in natural and elegant ways.
Now we fulfill our promise by adding support for
the ``exactly-$n$-times'' bounded regular expression $r^{\{n\}}$.
We add clauses in our derivatives-based lexing algorithms (with simplifications)
introduced in chapter \ref{Bitcoded2}.
\subsection{Augmented Definitions}
There are a number of definitions that needs to be augmented.
The most notable one would be the POSIX rules for $r^{\{n\}}$:
\begin{mathpar}
\inferrule{v \in vs}{\textit{Stars} place holder}
\end{mathpar}
\subsection{Proofs for the Augmented Lexing Algorithm}
We need to maintain two proofs with the additional $r^{\{n\}}$
construct: the
correctness proof in chapter \ref{Bitcoded2},
and the finiteness proof in chapter \ref{Finite}.
\subsubsection{Correctness Proof Augmentation}
The correctness of $\textit{lexer}$ and $\textit{blexer}$ with bounded repetitions
have been proven by Ausaf and Urban\cite{AusafDyckhoffUrban2016}.
As they have commented, once the definitions are in place,
the proofs given for the basic regular expressions will extend to
bounded regular expressions, and there are no ``surprises''.
We confirm this point because the correctness theorem would also
extend without surprise to $\blexersimp$.
The rewrite rules such as $\rightsquigarrow$, $\stackrel{s}{\rightsquigarrow}$ and so on
do not need to be changed,
and only a few lemmas such as lemma \ref{fltsPreserves} need to be adjusted to
add one more line which can be solved by sledgehammer
to solve the $r^{\{n\}}$ inductive case.
\subsubsection{Finiteness Proof Augmentation}
The bounded repetitions are
very similar to stars, and therefore the treatment
is similar, with minor changes to handle some slight complications
when the counter reaches 0.
The exponential growth is similar:
\begin{center}
\begin{tabular}{ll}
$r^{\{n\}} $ & $\longrightarrow_{\backslash c}$\\
$(r\backslash c) \cdot
r^{\{n - 1\}}*$ & $\longrightarrow_{\backslash c'}$\\
\\
$r \backslash cc' \cdot r^{\{n - 2\}}* +
r \backslash c' \cdot r^{\{n - 1\}}*$ &
$\longrightarrow_{\backslash c''}$\\
\\
$(r_1 \backslash cc'c'' \cdot r^{\{n-3\}}* +
r \backslash c''\cdot r^{\{n-1\}}) +
(r \backslash c'c'' \cdot r^{\{n-2\}}* +
r \backslash c'' \cdot r^{\{n-1\}}*)$ &
$\longrightarrow_{\backslash c'''}$ \\
\\
$\ldots$\\
\end{tabular}
\end{center}
Again, we assume that $r\backslash c$, $r \backslash cc'$ and so on
are all nullable.
The flattened list of terms for $r^{\{n\}} \backslash_{rs} s$
\begin{center}
$[r_1 \backslash cc'c'' \cdot r^{\{n-3\}}*,\;
r \backslash c''\cdot r^{\{n-1\}}, \;
r \backslash c'c'' \cdot r^{\{n-2\}}*, \;
r \backslash c'' \cdot r^{\{n-1\}}*,\; \ldots ]$
\end{center}
that comes from
\begin{center}
$(r_1 \backslash cc'c'' \cdot r^{\{n-3\}}* +
r \backslash c''\cdot r^{\{n-1\}}) +
(r \backslash c'c'' \cdot r^{\{n-2\}}* +
r \backslash c'' \cdot r^{\{n-1\}}*)+ \ldots$
\end{center}
are made of sequences with different tails, where the counters
might differ.
The observation for maintaining the bound is that
these counters never exceed $n$, the original
counter. With the number of counters staying finite,
$\rDistinct$ will deduplicate and keep the list finite.
We introduce this idea as a lemma once we describe all
the necessary helper functions.
Similar to the star case, we want
\begin{center}
$\rderssimp{r^{\{n\}}}{s} = \rsimp{\sum rs}$.
\end{center}
where $rs$
shall be in the form of
$\map \; f \; Ss$, where $f$ is a function and
$Ss$ a list of objects to act on.
For star, the object's datatype is string.
The list of strings $Ss$
is generated using functions
$\starupdate$ and $\starupdates$.
The function that takes a string and returns a regular expression
is the anonymous function $
(\lambda s'. \; r\backslash s' \cdot r^{\{m\}})$.
In the NTIMES setting,
the $\starupdate$ and $\starupdates$ functions are replaced by
$\textit{nupdate}$ and $\textit{nupdates}$:
\begin{center}
\begin{tabular}{lcl}
$\nupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
$\nupdate \; c \; r \;
(\Some \; (s, \; n + 1) \; :: \; Ss)$ & $\dn$ & %\\
$\textit{if} \;
(\rnullable \; (r \backslash_{rs} s))$ \\
& & $\;\;\textit{then}
\;\; \Some \; (s @ [c], n + 1) :: \Some \; ([c], n) :: (
\nupdate \; c \; r \; Ss)$ \\
& & $\textit{else} \;\; \Some \; (s @ [c], n+1) :: (
\nupdate \; c \; r \; Ss)$\\
$\nupdate \; c \; r \; (\textit{None} :: Ss)$ & $\dn$ &
$(\None :: \nupdate \; c \; r \; Ss)$\\
& & \\
%\end{tabular}
%\end{center}
%\begin{center}
%\begin{tabular}{lcl}
$\nupdates \; [] \; r \; Ss$ & $\dn$ & $Ss$\\
$\nupdates \; (c :: cs) \; r \; Ss$ & $\dn$ & $\nupdates \; cs \; r \; (
\nupdate \; c \; r \; Ss)$
\end{tabular}
\end{center}
\noindent
which take into account when a subterm
\begin{center}
$r \backslash_s s \cdot r^{\{n\}}$
\end{center}
counter $n$
is 0, and therefore expands to
\begin{center}
$r \backslash_s (s@[c]) \cdot r^{\{n\}} \;+
\; \ZERO$
\end{center}
after taking a derivative.
The object now has type
\begin{center}
$\textit{option} \;(\textit{string}, \textit{nat})$
\end{center}
and therefore the function for converting such an option into
a regular expression term is called $\opterm$:
\begin{center}
\begin{tabular}{lcl}
$\opterm \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
& & $\;\;\Some \; (s, n) \Rightarrow
(r\backslash_{rs} s)\cdot r^{\{n\}}$\\
& & $\;\;\None \Rightarrow
\ZERO$\\
\end{tabular}
\end{center}
\noindent
Put together, the list $\map \; f \; Ss$ is instantiated as
\begin{center}
$\map \; (\opterm \; r) \; (\nupdates \; s \; r \;
[\Some \; ([c], n)])$.
\end{center}
For the closed form to be bounded, we would like
simplification to be applied to each term in the list.
Therefore we introduce some variants of $\opterm$,
which help conveniently express the rewriting steps
needed in the closed form proof.
\begin{center}
\begin{tabular}{lcl}
$\optermOsimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
& & $\;\;\Some \; (s, n) \Rightarrow
\textit{rsimp} \; ((r\backslash_{rs} s)\cdot r^{\{n\}})$\\
& & $\;\;\None \Rightarrow
\ZERO$\\
\\
$\optermosimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
& & $\;\;\Some \; (s, n) \Rightarrow
(\textit{rsimp} \; (r\backslash_{rs} s))
\cdot r^{\{n\}}$\\
& & $\;\;\None \Rightarrow
\ZERO$\\
\\
$\optermsimp \; r \; SN$ & $\dn$ & $\textit{case} \; SN\; of$\\
& & $\;\;\Some \; (s, n) \Rightarrow
(r\backslash_{rsimps} s)\cdot r^{\{n\}}$\\
& & $\;\;\None \Rightarrow
\ZERO$\\
\end{tabular}
\end{center}
For a list of
$\textit{option} \;(\textit{string}, \textit{nat})$ elements,
we define the highest power for it recursively:
\begin{center}
\begin{tabular}{lcl}
$\hpa \; [] \; n $ & $\dn$ & $n$\\
$\hpa \; (\None :: os) \; n $ & $\dn$ & $\hpa \; os \; n$\\
$\hpa \; (\Some \; (s, n) :: os) \; m$ & $\dn$ &
$\hpa \;os \; (\textit{max} \; n\; m)$\\
\\
$\hpower \; rs $ & $\dn$ & $\hpa \; rs \; 0$\\
\end{tabular}
\end{center}
Now the intuition that an NTIMES regular expression's power
does not increase can be easily expressed as
\begin{lemma}\label{nupdatesMono2}
$\hpower \; (\nupdates \;s \; r \; [\Some \; ([c], n)]) \leq n$
\end{lemma}
\begin{proof}
Note that the power is non-increasing after a $\nupdate$ application:
\begin{center}
$\hpa \;\; (\nupdate \; c \; r \; Ss)\;\; m \leq
\hpa\; \; Ss \; m$.
\end{center}
This is also the case for $\nupdates$:
\begin{center}
$\hpa \;\; (\nupdates \; s \; r \; Ss)\;\; m \leq
\hpa\; \; Ss \; m$.
\end{center}
Therefore we have that
\begin{center}
$\hpower \;\; (\nupdates \; s \; r \; Ss) \leq
\hpower \;\; Ss$
\end{center}
which leads to the lemma being proven.
\end{proof}
We also define the inductive rules for
the shape of derivatives of the NTIMES regular expressions:\\[-3em]
\begin{center}
\begin{mathpar}
\inferrule{\mbox{}}{\cbn \;\ZERO}
\inferrule{\mbox{}}{\cbn \; \; r_a \cdot (r^{\{n\}})}
\inferrule{\cbn \; r_1 \;\; \; \cbn \; r_2}{\cbn \; r_1 + r_2}
\inferrule{\cbn \; r}{\cbn \; r + \ZERO}
\end{mathpar}
\end{center}
\noindent
A derivative of NTIMES fits into the shape described by $\cbn$:
\begin{lemma}\label{ntimesDersCbn}
$\cbn \; ((r' \cdot r^{\{n\}}) \backslash_{rs} s)$ holds.
\end{lemma}
\begin{proof}
By a reverse induction on $s$.
For the inductive case, note that if $\cbn \; r$ holds,
then $\cbn \; (r\backslash_r c)$ holds.
\end{proof}
In addition, for $\cbn$-shaped regular expressioins, one can flatten
them:
\begin{lemma}\label{ntimesHfauPushin}
If $\cbn \; r$ holds, then $\hflataux{r \backslash_r c} =
\textit{concat} \; (\map \; \hflataux{\map \; (\_\backslash_r c) \;
(\hflataux{r})})$
\end{lemma}
\begin{proof}
By an induction on the inductive cases of $\cbn$.
\end{proof}
This time we do not need to define the flattening functions for NTIMES only,
because $\hflat{\_}$ and $\hflataux{\_}$ work on NTIMES already:
\begin{lemma}\label{ntimesHfauInduct}
$\hflataux{( (r\backslash_r c) \cdot r^{\{n\}}) \backslash_{rsimps} s} =
\map \; (\opterm \; r) \; (\nupdates \; s \; r \; [\Some \; ([c], n)])$
\end{lemma}
\begin{proof}
By a reverse induction on $s$.
The lemma \ref{ntimesDersCbn} is used.
\end{proof}
\noindent
We have a recursive property for NTIMES with $\nupdate$
similar to that for STAR,
and one for $\nupdates $ as well:
\begin{lemma}\label{nupdateInduct1}
(i) $\textit{concat} \; (\map \; (\hflataux{\_} \circ (
\opterm \; r)) \; Ss) = \map \; (\opterm \; r) \; (\nupdate \;
c \; r \; Ss)$\\
(ii) $\textit{concat} \; (\map \; \hflataux{\_}\;
\map \; (\_\backslash_r x) \;
(\map \; (\opterm \; r) \; (\nupdates \; xs \; r \; Ss))) =
\map \; (\opterm \; r) \; (\nupdates \;(xs@[x]) \; r\;Ss)$ holds.
\end{lemma}
\begin{proof}
(i) is by an induction on $Ss$.
(ii) is by an induction on $xs$.
\end{proof}
The $\nString$ predicate is defined for conveniently
expressing that there are no empty strings in the
$\Some \;(s, n)$ elements generated by $\nupdate$:
\begin{center}
\begin{tabular}{lcl}
$\nString \; \None$ & $\dn$ & $ \textit{true}$\\
$\nString \; (\Some \; ([], n))$ & $\dn$ & $ \textit{false}$\\
$\nString \; (\Some \; (c::s, n))$ & $\dn$ & $ \textit{true}$\\
\end{tabular}
\end{center}
\begin{lemma}\label{nupdatesNonempty}
If for all elements $opt$ in $\textit{set} \; Ss$,
$\nString \; opt$ holds, the we have that
for all elements $opt$ in $\textit{set} \; (\nupdates \; s \; r \; Ss)$,
$\nString \; opt$ holds.
\end{lemma}
\begin{proof}
By an induction on $s$, where $Ss$ is set to vary over all possible values.
\end{proof}
\noindent
\begin{lemma}\label{ntimesClosedFormsSteps}
The following list of equalities or rewriting relations hold:\\
(i) $r^{\{n+1\}} \backslash_{rsimps} (c::s) =
\textit{rsimp} \; (\sum (\map \; (\opterm \;r \;\_) \; (\nupdates \;
s \; r \; [\Some \; ([c], n)])))$\\
(ii)
\begin{center}
$\sum (\map \; (\opterm \; r) \; (\nupdates \; s \; r \; [
\Some \; ([c], n)]))$ \\ $ \sequal$\\
$\sum (\map \; (\textit{rsimp} \circ (\opterm \; r))\; (\nupdates \;
s\;r \; [\Some \; ([c], n)]))$\\
\end{center}
(iii)
\begin{center}
$\sum \;(\map \; (\optermosimp \; r) \; (\nupdates \; s \; r\; [\Some \;
([c], n)]))$\\
$\sequal$\\
$\sum \;(\map \; (\optermsimp r) \; (\nupdates \; s \; r \; [\Some \;
([c], n)])) $\\
\end{center}
(iv)
\begin{center}
$\sum \;(\map \; (\optermosimp \; r) \; (\nupdates \; s \; r\; [\Some \;
([c], n)])) $ \\ $\sequal$\\
$\sum \;(\map \; (\optermOsimp r) \; (\nupdates \; s \; r \; [\Some \;
([c], n)])) $\\
\end{center}
(v)
\begin{center}
$\sum \;(\map \; (\optermOsimp r) \; (\nupdates \; s \; r \; [\Some \;
([c], n)])) $ \\ $\sequal$\\
$\sum \; (\map \; (\textit{rsimp} \circ (\opterm \; r)) \;
(\nupdates \; s \; r \; [\Some \; ([c], n)]))$
\end{center}
\end{lemma}
\begin{proof}
Routine.
(iii) and (iv) make use of the fact that all the strings $s$
inside $\Some \; (s, m)$ which are elements of the list
$\nupdates \; s\;r\;[\Some\; ([c], n)]$ are non-empty,
which is from lemma \ref{nupdatesNonempty}.
Once the string in $o = \Some \; (s, n)$ is
nonempty, $\optermsimp \; r \;o$,
$\optermosimp \; r \; o$ and $\optermosimp \; \; o$ are guaranteed
to be equal.
\end{proof}
\begin{theorem}\label{ntimesClosedForm}
The derivative of $r^{\{n+1\}}$ can be described as an alternative
containing a list
of terms:\\
$r^{\{n+1\}} \backslash_{rsimps} (c::s) = \textit{rsimp} \; (
\sum (\map \; (\optermsimp \; r) \; (\nupdates \; s \; r \;
[\Some \; ([c], n)])))$
\end{theorem}
\begin{proof}
By the rewriting steps described in lemma \ref{ntimesClosedFormsSteps}.
\end{proof}
\begin{lemma}\label{nupdatesNLeqN}
For an element $o$ in $\textit{set} \; (\nupdates \; s \; r \;
[\Some \; ([c], n)])$, either $o = \None$, or $o = \Some
\; (s', m)$ for some string $s'$ and number $m \leq n$.
\end{lemma}
\begin{lemma}\label{ntimesClosedFormListElemShape}
For any element $r'$ in $\textit{set} \; (\map \; (\optermsimp \; r) \; (
\nupdates \; s \; r \; [\Some \; ([c], n)]))$,
we have that $r'$ is either $\ZERO$ or $r \backslash_{rsimps} s' \cdot
r^{\{m\}}$ for some string $s'$ and number $m \leq n$.
\end{lemma}
\begin{proof}
Using lemma \ref{nupdatesNLeqN}.
\end{proof}
\begin{theorem}\label{ntimesClosedFormBounded}
Assuming that for any string $s$, $\llbracket r \backslash_{rsimps} s
\rrbracket_r \leq N$ holds, then we have that\\
$\llbracket r^{\{n+1\}} \backslash_{rsimps} s \rrbracket_r \leq
\textit{max} \; (c_N+1)* (N + \llbracket r^{\{n\}} \rrbracket+1)$,
where $c_N = \textit{card} \; (\textit{sizeNregex} \; (
N + \llbracket r^{\{n\}} \rrbracket_r+1))$.
\end{theorem}
\begin{proof}
We have that for all regular expressions $r'$ in $\textit{set} \; (\map \; (\optermsimp \; r) \; (
\nupdates \; s \; r \; [\Some \; ([c], n)]))$,
$r'$'s size is less than or equal to $N + \llbracket r^{\{n\}}
\rrbracket_r + 1$
because $r'$ can only be either a $\ZERO$ or $r \backslash_{rsimps} s' \cdot
r^{\{m\}}$ for some string $s'$ and number
$m \leq n$ (lemma \ref{ntimesClosedFormListElemShape}).
In addition, we know that the list
$\map \; (\optermsimp \; r) \; (
\nupdates \; s \; r \; [\Some \; ([c], n)])$'s size is at most
$c_N = \textit{card} \;
(\sizeNregex \; ((N + \llbracket r^{\{n\}} \rrbracket) + 1))$.
This gives us $\llbracket \llbracket r \backslash_{rsimps} \;s \llbracket_r
\leq N * c_N$.
\end{proof}
Assuming we have that
\begin{center}
$\rderssimp{r^*}{s} = \rsimp{(\sum \map \; (\lambda s'. r\backslash s' \cdot r^*) \; Ss)}$.
\end{center}
holds.
The idea of $\starupdate$ and $\starupdates$
is to update $Ss$ when another
derivative is taken on $\rderssimp{r^*}{s}$
w.r.t a character $c$ and a string $s'$
respectively.
Both $\starupdate$ and $\starupdates$ take three arguments as input:
the new character $c$ or string $s$ to take derivative with,
the regular expression
$r$ under the star $r^*$, and the
list of strings $Ss$ for the derivative $r^* \backslash s$
up until this point
such that
\begin{center}
$(r^*) \backslash s = \sum_{s' \in sSet} (r\backslash s') \cdot r^*$
\end{center}
is satisfied.
Functions $\starupdate$ and $\starupdates$ characterise what the
star derivatives will look like once ``straightened out'' into lists.
The helper functions for such operations will be similar to
$\sflat{\_}$, $\sflataux{\_}$ and $\sflataux{\_}$, which we defined for sequence.
We use similar symbols to denote them, with a $*$ subscript to mark the difference.
\begin{center}
\begin{tabular}{lcl}
$\hflataux{r_1 + r_2}$ & $\dn$ & $\hflataux{r_1} @ \hflataux{r_2}$\\
$\hflataux{r}$ & $\dn$ & $[r]$
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{lcl}
$\hflat{r_1 + r_2}$ & $\dn$ & $\sum (\hflataux {r_1} @ \hflataux {r_2}) $\\
$\hflat{r}$ & $\dn$ & $r$
\end{tabular}
\end{center}
\noindent
These definitions are tailor-made for dealing with alternatives that have
originated from a star's derivatives.
A typical star derivative always has the structure of a balanced binary tree:
\begin{center}
$(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') +
(r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) $
\end{center}
All of the nested structures of alternatives
generated from derivatives are binary, and therefore
$\hflat{\_}$ and $\hflataux{\_}$ only deal with binary alternatives.
$\hflat{\_}$ ``untangles'' like the following:
\[
\sum ((r_1 + r_2) + (r_3 + r_4)) + \ldots \;
\stackrel{\hflat{\_}}{\longrightarrow} \;
\RALTS{[r_1, r_2, \ldots, r_n]}
\]
Here is a lemma stating the recursive property of $\starupdate$ and $\starupdates$,
with the helpers $\hflat{\_}$ and $\hflataux{\_}$\footnote{The function $\textit{concat}$ takes a list of lists
and merges each of the element lists to form a flattened list.}:
\begin{lemma}\label{stupdateInduct1}
\mbox
For a list of strings $Ss$, the following hold.
\begin{itemize}
\item
If we do a derivative on the terms
$r\backslash_r s \cdot r^*$ (where $s$ is taken from the list $Ss$),
the result will be the same as if we apply $\starupdate$ to $Ss$.
\begin{center}
\begin{tabular}{c}
$\textit{concat} \; (\map \; (\hflataux{\_} \circ ( (\_\backslash_r x)
\circ (\lambda s.\;\; (r \backslash_r s) \cdot r^*)))\; Ss )\;
$\\
\\
$=$ \\
\\
$\map \; (\lambda s. (r \backslash_r s) \cdot (r^*)) \;
(\starupdate \; x \; r \; Ss)$
\end{tabular}
\end{center}
\item
$\starupdates$ is ``composable'' w.r.t a derivative.
It piggybacks the character $x$ to the tail of the string
$xs$.
\begin{center}
\begin{tabular}{c}
$\textit{concat} \; (\map \; \hflataux{\_} \;
(\map \; (\_\backslash_r x) \;
(\map \; (\lambda s.\;\; (r \backslash_r s) \cdot
(r^*) ) \; (\starupdates \; xs \; r \; Ss))))$\\
\\
$=$\\
\\
$\map \; (\lambda s.\;\; (r\backslash_r s) \cdot (r^*)) \;
(\starupdates \; (xs @ [x]) \; r \; Ss)$
\end{tabular}
\end{center}
\end{itemize}
\end{lemma}
\begin{proof}
Part 1 is by induction on $Ss$.
Part 2 is by induction on $xs$, where $Ss$ is left to take arbitrary values.
\end{proof}
Like $\textit{createdBySequence}$, we need
a predicate for ``star-created'' regular expressions:
\begin{center}
\begin{mathpar}
\inferrule{\mbox{}}{ \textit{createdByStar}\; \RSEQ{ra}{\RSTAR{rb}} }
\inferrule{ \textit{createdByStar} \; r_1\; \land \; \textit{createdByStar} \; r_2 }{\textit{createdByStar} \; (r_1 + r_2) }
\end{mathpar}
\end{center}
\noindent
All regular expressions created by taking derivatives of
$r_1 \cdot (r_2)^*$ satisfy the $\textit{createdByStar}$ predicate:
\begin{lemma}\label{starDersCbs}
$\textit{createdByStar} \; ((r_1 \cdot r_2^*) \backslash_r s) $ holds.
\end{lemma}
\begin{proof}
By a reverse induction on $s$.
\end{proof}
If a regular expression conforms to the shape of a star's derivative,
then we can push an application of $\hflataux{\_}$ inside a derivative of it:
\begin{lemma}\label{hfauPushin}
If $\textit{createdByStar} \; r$ holds, then
\begin{center}
$\hflataux{r \backslash_r c} = \textit{concat} \; (
\map \; \hflataux{\_} (\map \; (\_\backslash_r c) \;(\hflataux{r})))$
\end{center}
holds.
\end{lemma}
\begin{proof}
By an induction on the inductivev cases of $\textit{createdByStar}$.
\end{proof}
%This is not entirely true for annotated regular expressions:
%%TODO: bsimp bders \neq bderssimp
%\begin{center}
% $(1+ (c\cdot \ASEQ{bs}{c^*}{c} ))$
%\end{center}
%For bit-codes, the order in which simplification is applied
%might cause a difference in the location they are placed.
%If we want something like
%\begin{center}
% $\bderssimp{r}{s} \myequiv \bsimp{\bders{r}{s}}$
%\end{center}
%Some "canonicalization" procedure is required,
%which either pushes all the common bitcodes to nodes
%as senior as possible:
%\begin{center}
% $_{bs}(_{bs_1 @ bs'}r_1 + _{bs_1 @ bs''}r_2) \rightarrow _{bs @ bs_1}(_{bs'}r_1 + _{bs''}r_2) $
%\end{center}
%or does the reverse. However bitcodes are not of interest if we are talking about
%the $\llbracket r \rrbracket$ size of a regex.
%Therefore for the ease and simplicity of producing a
%proof for a size bound, we are happy to restrict ourselves to
%unannotated regular expressions, and obtain such equalities as
%TODO: rsimp sflat
% The simplification of a flattened out regular expression, provided it comes
%from the derivative of a star, is the same as the one nested.
Now we introduce an inductive property
for $\starupdate$ and $\hflataux{\_}$.
\begin{lemma}\label{starHfauInduct}
If we do derivatives of $r^*$
with a string that starts with $c$,
then flatten it out,
we obtain a list
of the shape $\sum_{s' \in sS} (r\backslash_r s') \cdot r^*$,
where $sS = \starupdates \; s \; r \; [[c]]$. Namely,
\begin{center}
$\hflataux{(\rders{( (\rder{c}{r_0})\cdot(r_0^*))}{s})} =
\map \; (\lambda s_1. (r_0 \backslash_r s_1) \cdot (r_0^*)) \;
(\starupdates \; s \; r_0 \; [[c]])$
\end{center}
holds.
\end{lemma}
\begin{proof}
By an induction on $s$, the inductive cases
being $[]$ and $s@[c]$. The lemmas \ref{hfauPushin} and \ref{starDersCbs} are used.
\end{proof}
\noindent
$\hflataux{\_}$ has a similar effect as $\textit{flatten}$:
\begin{lemma}\label{hflatauxGrewrites}
$a :: rs \grewrites \hflataux{a} @ rs$
\end{lemma}
\begin{proof}
By induction on $a$. $rs$ is set to take arbitrary values.
\end{proof}
It is also not surprising that $\textit{rsimp}$ will cover
the effect of $\hflataux{\_}$:
\begin{lemma}\label{cbsHfauRsimpeq1}
$\rsimp{(r_1 + r_2)} = \rsimp{(\RALTS{\hflataux{r_1} @ \hflataux{r_2}})}$
\end{lemma}
\begin{proof}
By using the rewriting relation $\rightsquigarrow$
\end{proof}
And from this we obtain a proof that a star's derivative will be the same
as if it had all its nested alternatives created during deriving being flattened out:
For example,
\begin{lemma}\label{hfauRsimpeq2}
$\createdByStar{r} \implies \rsimp{r} = \rsimp{\RALTS{\hflataux{r}}}$
\end{lemma}
\begin{proof}
By structural induction on $r$, where the induction rules
are these of $\createdByStar{\_}$.
Lemma \ref{cbsHfauRsimpeq1} is used in the inductive case.
\end{proof}
%Here is a corollary that states the lemma in
%a more intuitive way:
%\begin{corollary}
% $\hflataux{r^* \backslash_r (c::xs)} = \map \; (\lambda s. (r \backslash_r s) \cdot
% (r^*))\; (\starupdates \; c\; r\; [[c]])$
%\end{corollary}
%\noindent
%Note that this is also agnostic of the simplification
%function we defined, and is therefore of more general interest.
Together with the rewriting relation
\begin{lemma}\label{starClosedForm6Hrewrites}
We have the following set of rewriting relations or equalities:
\begin{itemize}
\item
$\textit{rsimp} \; (r^* \backslash_r (c::s))
\sequal
\sum \; ( ( \sum (\lambda s. (r\backslash_r s) \cdot r^*) \; (
\starupdates \; s \; r \; [ c::[]] ) ) )$
\item
$r \backslash_{rsimp} (c::s) = \textit{rsimp} \; ( (
\sum ( (\map \; (\lambda s_1. (r\backslash s_1) \; r^*) \;
(\starupdates \;s \; r \; [ c::[] ])))))$
\item
$\sum ( (\map \; (\lambda s. (r\backslash s) \; r^*) \; Ss))
\sequal
\sum ( (\map \; (\lambda s. \textit{rsimp} \; (r\backslash s) \;
r^*) \; Ss) )$
\item
$\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss
\scfrewrites
\map \; (\lambda s. (\rsimp{r \backslash_r s}) \cdot (r^*)) \; Ss$
\item
$( ( \sum ( ( \map \ (\lambda s. \;\;
(\textit{rsimp} \; (r \backslash_r s)) \cdot r^*) \; (\starupdates \;
s \; r \; [ c::[] ])))))$\\
$\sequal$\\
$( ( \sum ( ( \map \ (\lambda s. \;\;
( r \backslash_{rsimp} s)) \cdot r^*) \; (\starupdates \;
s \; r \; [ c::[] ]))))$\\
\end{itemize}
\end{lemma}
\begin{proof}
Part 1 leads to part 2.
The rest of them are routine.
\end{proof}
\noindent
Next the closed form for star regular expressions can be derived:
\begin{theorem}\label{starClosedForm}
$\rderssimp{r^*}{c::s} =
\rsimp{
(\sum (\map \; (\lambda s. (\rderssimp{r}{s})\cdot r^*) \;
(\starupdates \; s\; r \; [[c]])
)
)
}
$
\end{theorem}
\begin{proof}
By an induction on $s$.
The lemmas \ref{rsimpIdem}, \ref{starHfauInduct}, \ref{starClosedForm6Hrewrites}
and \ref{hfauRsimpeq2}
are used.
In \ref{starClosedForm6Hrewrites}, the equalities are
used to link the LHS and RHS.
\end{proof}
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 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}