lexing: comparison ChengsongTanPhdThesis/Chapters/Cubic.tex

equal deleted inserted replaced

-:96e009a446d5
+:d50a309a0645
 % Chapter Template
-\chapter{A Better Bound and Other Extensions} % Main chapter title
+%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 intend to formalise this part, which
+We make a conjecture that the finite
-we have not been able to finish due to time constraints of the PhD.
+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
+%Unfortunately we did not have time to
-work out the proofs, like in
+%work out the proofs, like in
-the previous chapters.
+%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
+hold.
-is still future work.
+%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.\\
+Animirov's partial derivatives.
-%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^*
 \]
 $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}
-It is characterised as the $LD$
+This is characterised as the $LD$
-rewrite rule in figure \ref{rrewriteRules}.\\
+rewrite rule in figure \ref{rrewriteRules}.
-The problem , however, is that identical components
+The problem, however, is that identical components
-in two slightly different regular expressions cannot be removed.
+in two slightly different regular expressions cannot be removed
-Consider the simplification
+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 $(a+\ldots)\cdot r_1$ is deleted in the right alternative.
+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,
+cannot be omitted, if we want to have a better bound.
-as without it the size of derivatives can still
+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,
+and set $n$ to a relatively small number like $n=5$, then we get the following
-we get exponential growth:
+exponential growth:
 \begin{figure}[H]
 \centering
 \begin{tikzpicture}
 \begin{axis}[
 %xlabel={$n$},
 ylabel={size},
 ]
 \addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};
 \end{axis}
 \end{tikzpicture}
-\caption{Size of derivatives of $\blexersimp$ for matching
+\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
 rule
 \[
 	(a+b+d) \cdot r_1  \longrightarrow a \cdot r_1 + b \cdot r_1 + d \cdot r_1
 \]
 \noindent
-in our $\simp$ function,
+which pushes the sequence into the alternatives
-so that it makes the simplification in \eqref{eqn:partialDedup} possible.
+in our $\simp$ function.
-Translating the rule into our $\textit{bsimp}$ function simply
+This would then make the simplification shown in \eqref{eqn:partialDedup} possible.
-involves adding a new clause to the $\textit{bsimp}_{ASEQ}$ function:
+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 (
 &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow   _{bs}a_1' \cdot a_2'$ \\
 	\end{tabular}
 \end{center}
 \noindent
 Unfortunately,
-if we introduce them in our
+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}
 	$\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
+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.
-However this violates the POSIX rules.
+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 becomes a regular expression with a
+which is a regular expression with a
-quite different structure--the original
+quite different meaning: the original regular expression
-was a sequence, and now it becomes an alternative.
+is a sequence, but the simplified regular expression is an alternative.
-With an alternative the maximal munch rule no longer works.\\
+With an alternative the maximal munch rule no longer works.
-A method to reconcile this is to do the
+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}
+%\begin{center}
-	$rs_a@[a]@rs_c$
+%	$rs_a@[a]@rs_c$
-\end{center}
+%\end{center}
-in the alternative
+inside alternatives
 \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:
+we allow the following more general rewrite rule:
-\begin{figure}[H]
+\begin{equation}
-\begin{mathpar}
+\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}
+%\end{mathpar}
-\caption{The rule capturing the pruning simplification needed to achieve
+%\caption{The rule capturing the pruning simplification needed to achieve
-a cubic bound}
+%a cubic bound}
-\label{fig:cubicRule}
+\end{equation}
-\end{figure}
+\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$, removing components in $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}
 \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
+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
+We implemented the
-function $\textit{prune}$ in Scala:
+function $\textit{prune}$ in Scala (see figure \ref{fig:pruneFunc})
-\begin{figure}[H]
+The function $\textit{prune}$
-\begin{lstlisting}
+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
 }
 //this does the duplicate component removal task
 case r => if(acc(erase(r))) AZERO else r
 }
 \end{lstlisting}
-\caption{The function $\textit{prune}$ }
+\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
-The function $\textit{prune}$
-is a stronger version of $\textit{distinctBy}$.
+\begin{figure}
-It does not just walk through a list looking for exact duplicates,
+\begin{lstlisting}[numbers=left]
-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}
 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)
 if (r == tail)
 ONE
 else {
 r match {
 case SEQ(r1, r2) =>
-if(r2 == tail)
+if(r2 == tail) r1 else ZERO
-r1
-else
-ZERO
 case r => ZERO
 }
 }
 \end{lstlisting}
-\caption{The helper functions of $\textit{prune}$}
+\caption{The helper functions of $\textit{prune}$ XXX.}
 \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 for $\textit{prune}$.
+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.
 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 we will be comparing
+accumulators as well, otherwise the deletion will not work.
-apples with oranges.
 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 $b\cdot g$ only.
+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}
+\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
 )
 }
 }
 \end{lstlisting}
-\caption{A Stronger Version of $\textit{distinctBy}$}
+\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.
 }
 \end{lstlisting}
 \end{figure}
 \noindent
 We call this lexer $\blexerStrong$.
-This version is able to drastically reduce the
+This version is able to reduce the
-internal data structure size which
+size of the derivatives which
-otherwise could
+otherwise
-trigger exponential behaviours in
+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}[
 \addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};
 \end{axis}
 \end{tikzpicture}\\
 \multicolumn{2}{l}{}
 \end{tabular}
-\caption{Runtime for matching
+\caption{}\label{fig:aaaaaStarStar}
-	$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$ with strings
-	   of the form $\protect\underbrace{aa..a}_{n}$.}\label{fig:aaaaaStarStar}
 \end{figure}
 \noindent
-We would like to preserve the correctness like the one
+We hope the correctness is preserved.
-we had for $\blexersimp$:
+%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 \ref{fig:cubicRule} .
+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.
 $\bdersStrongs$.
 \subsection{Antimirov's partial derivatives}
 Partial derivatives were first introduced by
 Antimirov \cite{Antimirov95}.
-Partial derivatives are very similar
+They are very similar
 to Brzozowski derivatives,
-but splits children of alternative regular expressions into
+but split children of alternative regular expressions into
 multiple independent terms. This means the output of
-partial derivatives become a
+partial derivatives is a
-set of regular expressions:
+set of regular expressions, defined as follows
 \begin{center}
-	\begin{tabular}{lcl}
+	\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_2 \;$ & $ \textit{if} \; \; \nullable\; r_1$\\
-		      & & $(\partial_x \; r_1)\cdot r_2 \quad\quad
+				      & & $(\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(\ONE)$ & $=$ & $\varnothing$\\
 		$\partial_x(\ZERO)$ & $\dn$ & $\varnothing$\\
 	\end{tabular}
 \end{center}
 \noindent
-The $\cdot$ between for example
+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,
+because they are sets.
-For example, to compute what regular expression $x^*(xx + y)^*$'s
+For example, to compute what the derivative of the regular expression
-derivative w.r.t. $x$ is, one can compute a partial derivative
+$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'
 \]
-Given an alphabet $\Sigma$, we denote the set of all possible strings
+Suppose an alphabet $\Sigma$, we use $\Sigma^*$ for the set of all possible strings
-from this alphabet as $\Sigma^*$.
+from the alphabet.
-The set of all possible partial derivatives is defined
+The set of all possible partial derivatives is then defined
-as the union of derivatives w.r.t all the strings in the universe:
+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 the derivatives
+Consider now again our pathological case where we apply the more
-grow with a rather aggressive simplification
+aggressive
+simplification
 \begin{center}
 	$((a^* + (aa)^* + \ldots + (\underbrace{a\ldots a}_{n a's})^* )^*)^*$
 \end{center}
-example, if we denote this regular expression as $r$,
+let use abbreviate theis regular expression with $r$,
-we have that
+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}
-with exactly $n * (n + 1) / 2$ terms.
+The union on the right-hand-side has $n * (n + 1) / 2$ terms.
-This is in line with our speculation that only $n*(n+1)/2$ terms are
+This leads us to believe that the maximum number of terms needed
-needed. We conjecture that $\bsimpStrong$ is also able to achieve this
+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
+	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
-because our \ref{fig:cubicRule} will keep only one copy of each term,
+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}$
+%We might need to adjust $\textit{prune}$
-slightly to make sure all duplicate terms are eliminated,
+%slightly to make sure all duplicate terms are eliminated,
-which should be doable.
+%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 proofs. \footnote{https://www.isa-afp.org/entries/Myhill-Nerode.html}
+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 yield us also a cubic bound for our $\blexerStrong$ algorithm:
+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.

changeset 630	d50a309a0645
parent 628	7af4e2420a8c
child 638	dd9dde2d902b