lexing: comparison thys2/Paper/Paper.thy

equal deleted inserted replaced

-:2416fdec6396
+:14c558ae0b09
 notation (latex output)
 der_syn ("_\\_" [79, 1000] 76) and
 ders_syn ("_\\_" [79, 1000] 76) and
 bder_syn ("_\\_" [79, 1000] 76) and
 bders ("_\\_" [79, 1000] 76) and
-bders_simp ("_\\\<^sub>s\<^sub>i\<^sub>m\<^sub>p _" [79, 1000] 76) and
+bders_simp ("_\\\<^sub>b\<^sub>s\<^sub>i\<^sub>m\<^sub>p _" [79, 1000] 76) and
 ZERO ("\<^bold>0" 81) and
 ONE ("\<^bold>1" 81) and
 CH ("_" [1000] 80) and
 ALT ("_ + _" [77,77] 78) and
 bsimp_ASEQ ("bsimpSEQ _ _ _" [10,1000,1000] 80) and
 bmkeps ("bmkeps _" [1000] 80) and
 srewrite ("_\<^latex>\<open>\\mbox{$\\,\\stackrel{s}{\\leadsto}$}\<close> _" [71, 71] 80) and
 rrewrites ("_ \<^latex>\<open>\\mbox{$\\,\\leadsto^*$}\<close> _" [71, 71] 80) and
+srewrites ("_ \<^latex>\<open>\\mbox{$\\,\\stackrel{s}{\\leadsto}^*$}\<close> _" [71, 71] 80) and
 blexer_simp ("blexer\<^sup>+" 1000)
 lemma better_retrieve:
 shows "rs \<noteq> Nil ==> retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v"
 does not achieve the intended objective with bitcoded regular expressions.  The
 reason is that in the bitcoded setting, each copy generally has a
 different bitcode annotation---so @{text nub} would never ``fire''.
 Inspired by Scala's library for lists, we shall instead use a @{text
 distinctBy} function that finds duplicates under an erasing function
-that deletes bitcodes.
+which deletes bitcodes.
 We shall also introduce our own argument and definitions for
 establishing the correctness of the bitcoded algorithm when
 simplifications are included.\medskip
 \noindent In this paper, we shall first briefly introduce the basic notions
 	lexing acquired its name from the fact that the corresponding
 	rules were described as part of the POSIX specification for
 	Unix-like operating systems \cite{POSIX}.} Sometimes these
 informal rules are called \emph{maximal much rule} and \emph{rule priority}.
 One contribution of our earlier paper is to give a convenient
-specification for what a POSIX value is (the inductive rules are shown in
+specification for what POSIX values are (the inductive rules are shown in
 Figure~\ref{POSIXrules}).
 \begin{figure}[t]
 \begin{center}
 \begin{tabular}{c}
 where the path from the left to the right involving @{term derivatives}/@{const
 nullable} is the first phase of the algorithm (calculating successive
 \Brz's derivatives) and @{const mkeps}/@{text inj}, the path from right to
 left, the second phase. The picture above shows the steps required when a
 regular expression, say @{text "r\<^sub>1"}, matches the string @{term
-"[a,b,c]"}. The lexing algorithm by Sulzmann and Lu can be defined as:
+"[a,b,c]"}. The first lexing algorithm by Sulzmann and Lu can be defined as:
 \begin{figure}[t]
 \begin{center}
 \begin{tikzpicture}[scale=2,node distance=1.3cm,
 every node/.style={minimum size=6mm}]
 \noindent
 In fact we have shown that in the success case the generated POSIX value $v$ is
 unique and in the failure case that there is no POSIX value $v$ that satisfies
 $(s, r) \rightarrow v$. While the algorithm is correct, it is excrutiatingly
-slow in cases where the derivatives grow arbitrarily (see example from the
+slow in cases where the derivatives grow arbitrarily (recall the example from the
 Introduction). However it can be used as a convenient reference point for the correctness
 proof of the second algorithm by Sulzmann and Lu, which we shall describe next.
 *}
 \noindent where @{text bs} stands for bitsequences; @{text r},
 @{text "r\<^sub>1"} and @{text "r\<^sub>2"} for bitcoded regular
 expressions; and @{text rs} for lists of bitcoded regular
 expressions. The binary alternative @{text "ALT bs r\<^sub>1 r\<^sub>2"}
 is just an abbreviation for \mbox{@{text "ALTs bs [r\<^sub>1, r\<^sub>2]"}}.
-For bitsequences we just use lists made up of the
+For bitsequences we use lists made up of the
 constants @{text Z} and @{text S}.  The idea with bitcoded regular
 expressions is to incrementally generate the value information (for
 example @{text Left} and @{text Right}) as bitsequences. For this
 Sulzmann and Lu define a coding
 function for how values can be coded into bitsequences.
 for any bit-sequence $bs$ and $\vdash v : r$. This property can be
 easily proved by induction on $\vdash v : r$.
 \end{proof}
 Sulzmann and Lu define the function \emph{internalise}
-in order to transform standard regular expressions into annotated
+in order to transform (standard) regular expressions into annotated
 regular expressions. We write this operation as $r^\uparrow$.
 This internalisation uses the following
 \emph{fuse} function.
 \begin{center}
 \end{tabular}
 \end{center}
 \noindent
 A regular expression can then be \emph{internalised} into a bitcoded
-regular expression as follows.
+regular expression as follows:
 \begin{center}
 \begin{tabular}{lcl}
 $(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\
 $(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
 transforms a bitcoded regular expression into a (standard) regular
 expression by just erasing the annotated bitsequences. We omit the
 straightforward definition. For defining the algorithm, we also need
 the functions \textit{bnullable} and \textit{bmkeps}, which are the
 ``lifted'' versions of \textit{nullable} and \textit{mkeps} acting on
-bitcoded regular expressions, instead of regular expressions.
+bitcoded regular expressions.
 %
 \begin{center}
 \begin{tabular}{@ {}c@ {}c@ {}}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 $\textit{bnullable}\,(\textit{ZERO})$ & $\dn$ & $\textit{false}$\\
 \noindent
 The key function in the bitcoded algorithm is the derivative of a
 bitcoded regular expression. This derivative calculates the
-derivative but at the same time also the incremental part of bitsequences
+derivative but at the same time also the incremental part of the bitsequences
 that contribute to constructing a POSIX value.
 \begin{center}
 \begin{tabular}{@ {}lcl@ {}}
 $(\textit{ZERO})\backslash c$ & $\dn$ & $\textit{ZERO}$ \\
 \end{proof}
 \noindent
 The only difficulty left for the correctness proof is that the bitcoded algorithm
 has only a ``forward phase'' where POSIX values are generated incrementally.
-We can achieve the same effect with @{text lexer} by stacking up injection
+We can achieve the same effect with @{text lexer} (which has two phases) by stacking up injection
 functions during the forward phase. An auxiliary function, called $\textit{flex}$,
-allows us to recast the rules of $\lexer$ (with its two phases) in terms of a single
+allows us to recast the rules of $\lexer$ in terms of a single
 phase and stacked up injection functions.
 \begin{center}
 \begin{tabular}{lcl}
 $\textit{flex}\;r\,f\,[]$ & $\dn$ & $f$\\
 \end{tabular}
 \end{center}
 \noindent
 The point of this function is that when
-reaching the end of the string, we just need to apply the stacked
+reaching the end of the string, we just need to apply the stacked up
 injection functions to the value generated by @{text mkeps}.
 Using this function we can recast the success case in @{text lexer}
 as follows:
 \begin{proposition}\label{flex}
 value generated by \textit{lexer} can also be obtained by a different
 method. While this different method is not efficient (we essentially
 need to traverse the string $s$ twice, once for building the
 derivative $r\backslash s$ and another time for stacking up injection
 functions using \textit{flex}), it helps us with proving
-that incrementally building up values generates the same result.
+that incrementally building up values in @{text blexer} generates the same result.
 This brings us to our main lemma in this section: if we calculate a
-derivative, say $r\backslash s$ and have a value, say $v$, inhabited
+derivative, say $r\backslash s$, and have a value, say $v$, inhabited
-by this derivative, then we can produce the result $\lexer$ generates
+by this derivative, then we can produce the result @{text lexer} generates
 by applying this value to the stacked-up injection functions
 that $\textit{flex}$ assembles. The lemma establishes that this is the same
 value as if we build the annotated derivative $r^\uparrow\backslash s$
 and then retrieve the corresponding bitcoded version, followed by a
 decoding step.
 \noindent
 With this lemma in place, we can prove the correctness of \textit{blexer}---it indeed
 produces the same result as \textit{lexer}.
-\begin{theorem}
+\begin{theorem}\label{thmone}
 $\textit{lexer}\,r\,s = \textit{blexer}\,r\,s$
 \end{theorem}
 \begin{proof}
 We can first expand both sides using Prop.~\ref{flex} and the
 \underbrace{\mbox{$(\ONE + \ONE{}a) \cdot (a + aa)^*$}}_{r} \;+\;
 ((a + aa)^* + \underbrace{\mbox{$(\ONE + \ONE{}a) \cdot (a + aa)^*$}}_{r})
 \end{equation}
 \noindent This is a simpler derivative, but unfortunately we
-cannot make further simplifications. This is a problem because
+cannot make any further simplifications. This is a problem because
 the outermost alternatives contains two copies of the same
-regular expression (underlined with $r$). The copies will
+regular expression (underlined with $r$). These copies will
-spawn new copies in later steps and they in turn further copies. This
+spawn new copies in later derivative steps and they in turn even more copies. This
-destroys an hope of taming the size of the derivatives.  But the
+destroys any hope of taming the size of the derivatives.  But the
 second copy of $r$ in \eqref{derivex} will never contribute to a
 value, because POSIX lexing will always prefer matching a string
-with the first copy. So in principle it could be removed.
+with the first copy. So it could be safely removed without affecting the correctness of the algorithm.
 The dilemma with the simple-minded
 simplification rules above is that the rule $r + r \Rightarrow r$
 will never be applicable because as can be seen in this example the
-regular expressions are separated by another sub-regular expression.
+regular expressions are not next to each other but separated by another regular expression.
 But here is where Sulzmann and Lu's representation of generalised
 alternatives in the bitcoded algorithm shines: in @{term
 "ALTs bs rs"} we can define a more aggressive simplification by
 recursively simplifying all regular expressions in @{text rs} and
 then analyse the resulting list and remove any duplicates.
-Another advantage is that the bitsequences in  bitcoded regular
+Another advantage with the bitsequences in  bitcoded regular
-expressions can be easily modified such that simplification does not
+expressions is that they can be easily modified such that simplification does not
 interfere with the value constructions. For example we can ``flatten'', or
 de-nest, @{text ALTs} as follows
 %
 \[
 @{term "ALTs bs\<^sub>1 ((ALTs bs\<^sub>2 rs\<^sub>2) # rs\<^sub>1)"}
 ensure that the correct value corresponding to the original (unsimplified)
 regular expression can still be extracted. %In this way the value construction
 %is not affected by simplification.
 However there is one problem with the definition for the more
-aggressive simlification rules by Sulzmann and Lu. Recasting
+aggressive simlification rules described by Sulzmann and Lu. Recasting
 their definition with our syntax they define the step of removing
 duplicates as
 %
 \[ @{text "bsimp (ALTs bs rs)"} \dn @{text "ALTs
 bs (nup (map bsimp rs))"}
 expressions in @{text rs} (using @{text map}) and then use
 Haskell's @{text nub}-function to remove potential
 duplicates. While this makes sense when considering the example
 shown in \eqref{derivex}, @{text nub} is the inappropriate
 function in the case of bitcoded regular expressions. The reason
-is that in general the n elements in @{text rs} will have a
+is that in general the elements in @{text rs} will have a
-different bitsequence annotated to it and in this way @{text nub}
+different annotated bitsequence and in this way @{text nub}
 will never find a duplicate to be removed. The correct way to
 handle this situation is to first \emph{erase} the regular
 expressions when comparing potential duplicates. This is inspired
 by Scala's list functions of the form \mbox{@{text "distinctBy rs f
 acc"}} where a function is applied first before two elements
 @{thm (lhs) distinctBy.simps(2)} & $\dn$ & @{thm (rhs) distinctBy.simps(2)}
 \end{tabular}
 \end{center}
 \noindent where we scan the list from left to right (because we
-have to remove later copies). In this function, @{text f} is a
+have to remove later copies). In @{text distinctBy}, @{text f} is a
 function and @{text acc} is an accumulator for regular
-expressions---essentially a set of elements we have already seen
+expressions---essentially a set of regular expression that we have already seen
 while scanning the list. Therefore we delete an element, say @{text x},
 from the list provided @{text "f x"} is already in the accumulator;
-otherwise we keep @{text x} and scan the rest of the list but now
+otherwise we keep @{text x} and scan the rest of the list but
-add @{text "f x"} as another element to @{text acc}. We will use
+add @{text "f x"} as another ``seen'' element to @{text acc}. We will use
-@{term distinctBy} where @{text f} is our erase functions, @{term "erase (DUMMY)"},
+@{term distinctBy} where @{text f} is the erase functions, @{term "erase (DUMMY)"},
 that deletes bitsequences from bitcoded regular expressions.
 This is clearly a computationally more expensive operation, than @{text nub},
 but is needed in order to make the removal of unnecessary copies
-to work.
+to work properly.
 Our simplification function depends on three helper functions, one is called
-@{text flts} and defined as follows:
+@{text flts} and analyses lists of regular expressions coming from alternatives.
+It is defined as follows:
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{thm (lhs) flts.simps(1)} & $\dn$ & @{thm (rhs) flts.simps(1)}\\
 @{thm (lhs) flts.simps(2)} & $\dn$ & @{thm (rhs) flts.simps(2)}\\
 @{thm (lhs) flts.simps(3)[of "bs'" "rs'"]} & $\dn$ & @{thm (rhs) flts.simps(3)[of "bs'" "rs'"]}\\
 \end{tabular}
 \end{center}
 \noindent
-The second clause removes all instances of @{text ZERO} in alternatives and
+The second clause of @{text flts} removes all instances of @{text ZERO} in alternatives and
 the second ``spills'' out nested alternatives (but retaining the
 bitsequence @{text "bs'"} accumulated in the inner alternative). There are
 some corner cases to be considered when the resulting list inside an alternative is
 empty or a singleton list. We take care of those cases in the
 @{text "bsimpALTs"} function; similarly we define a helper function that simplifies
 \end{tabular}
 \end{center}
 \noindent
 As far as we can see, our recursive function @{term bsimp} simplifies regular
-expressions as intended by Sulzmann and Lu. There is no point to apply the
+expressions as intended by Sulzmann and Lu. There is no point in applying the
-@{text bsimp}
+@{text bsimp} function repeatedly (like the simplification in their paper which needs to be
-function repeatedly (like the simplification in their paper which is applied
+applied until a fixpoint is reached) because we can show that @{term bsimp} is idempotent,
-until a fixpoint is reached), because we can show that it is idempotent, that is
+that is
 \begin{proposition}
-???
+@{term "bsimp (bsimp r) = bsimp r"}
 \end{proposition}
+\noindent
+This can be proved by induction on @{text r} but requires a detailed analysis
+that the de-nesting of alternatives always results in a flat list of regular
+expressions. We omit the details since it does not concern the correctness proof.
+Next we can include simplification after each derivative step leading to the
+following notion of bitcoded derivatives:
+\begin{center}
+\begin{tabular}{cc}
+\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+@{thm (lhs) bders_simp.simps(1)} & $\dn$ & @{thm (rhs) bders_simp.simps(1)}
+\end{tabular}
+&
+\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+@{thm (lhs) bders_simp.simps(2)} & $\dn$ & @{thm (rhs) bders_simp.simps(2)}
+\end{tabular}
+\end{tabular}
+\end{center}
+\noindent
+and use it in the improved lexing algorithm defined as
+\begin{center}
+\begin{tabular}{lcl}
+$\textit{blexer}^+\;r\,s$ & $\dn$ &
+$\textit{let}\;r_{der} = (r^\uparrow)\backslash_{bsimp}\, s\;\textit{in}$\\
+& & $\;\;\;\;\textit{if}\; \textit{bnullable}(r_{der}) \;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,r_{der})\,r
+\;\;\textit{else}\;\textit{None}$
+\end{tabular}
+\end{center}
+\noindent The remaining task is to show that @{term blexer} and
+@{term "blexer_simp"} generate the same answers.
+When we first
+attempted this proof we encountered a problem with the idea
+in Sulzmann and Lu's paper where the argument seems to be to appeal
+again to the @{text retrieve}-function defined for the unsimplified version
+of the algorithm. But
+this does not work, because desirable properties such as
+%
+\[
+@{text "retrieve r v = retrieve (bsimp r) v"}
+\]
+\noindent do not hold under simplification---this property
+essentially purports that we can retrieve the same value from a
+simplified version of the regular expression. To start with @{text retrieve}
+depends on the fact that the value @{text v} correspond to the
+structure of the regular exprssions---but the whole point of simplification
+is to ``destroy'' this structure by making the regular expression simpler.
+To see this consider the regular expression @{text "r = r' + 0"} and a corresponding
+value @{text "v = Left v'"}. If we annotate bitcodes to @{text "r"}, then
+we can use @{text retrieve} and @{text v} in order to extract a corresponding
+bitsequence. The reason that this works is that @{text r} is an alternative
+regular expression and @{text v} a corresponding value. However, if we simplify
+@{text r}, then @{text v} does not correspond to the shape of the regular
+expression anymore. So unless one can somehow
+synchronise the change in the simplified regular expressions with
+the original POSIX value, there is no hope of appealing to @{text retrieve} in the
+correctness argument for @{term blexer_simp}.
+We found it more helpful to introduce the rewriting systems shown in
+Figure~\ref{SimpRewrites}. The idea is to generate
+simplified regular expressions in small steps (unlike the @{text bsimp}-function which
+does the same in a big step), and show that each of
+the small steps preserves the bitcodes that lead to the final POSIX value.
+The rewrite system is organised such that $\leadsto$ is for bitcode regular
+expressions and $\stackrel{s}{\leadsto}$ for lists of bitcoded regular
+expressions. The former essentially implements the simplifications of
+@{text "bsimpSEQ"} and @{text flts}; while the latter implements the
+simplifications in @{text "bsimpALTs"}. We can show that any bitcoded
+regular expression reduces in one or more steps to the simplified
+regular expression generated by @{text bsimp}:
+\begin{lemma}\label{lemone}
+@{thm[mode=IfThen] rewrites_to_bsimp}
+\end{lemma}
+\begin{proof}
+By induction on @{text r}. For this we can use the properties
+@{thm fltsfrewrites} and @{thm ss6_stronger}. The latter uses
+repeated applications of the $LD$ rule which allows the removal
+of duplicates that can recognise the same strings.
+\end{proof}
+\noindent
+We can show that this rewrite system preserves @{term bnullable}, that
+is simplification, essentially, does not affect nullability:
 \begin{lemma}
 @{thm[mode=IfThen] bnullable0(1)[of "r\<^sub>1" "r\<^sub>2"]}
 \end{lemma}
+\begin{proof}
-\begin{lemma}
+Straightforward mutual induction on the definition of $\leadsto$ and $\stackrel{s}{\leadsto}$.
+The only interesting case is the rule $LD$ where the property holds since by the side-conditions of that rule the empty string will
+be in both @{text "L (rs\<^sub>a @ [r\<^sub>1] @ rs\<^sub>b @ [r\<^sub>2] @ rs\<^sub>c)"} and
+@{text "L (rs\<^sub>a @ [r\<^sub>1] @ rs\<^sub>b @ rs\<^sub>c)"}.
+\end{proof}
+\noindent
+From this, we can show that @{text bmkeps} will producte the same bitsequence
+as long as one of the bitcoded regular expressions in $\leadsto$ is nullable (this lemma
+establishes the missing fact we were not able to establish using @{text retrieve}, as suggested
+in the paper by Sulzmannn and Lu).
+\begin{lemma}\label{lemthree}
 @{thm[mode=IfThen] rewrite_bmkeps_aux(1)[of "r\<^sub>1" "r\<^sub>2"]}
 \end{lemma}
-\begin{lemma}
+\begin{proof}
-@{thm[mode=IfThen] rewrites_to_bsimp}
+By straightforward mutual induction on the definition of $\leadsto$ and $\stackrel{s}{\leadsto}$.
-\end{lemma}
+Again the only interesting case is the rule $LD$ where we need to ensure that
+\[
+@{text "bmkeps (rs\<^sub>a @ [r\<^sub>1] @ rs\<^sub>b @ [r\<^sub>2] @ rs\<^sub>c) =
+bmkeps (rs\<^sub>a @ [r\<^sub>1] @ rs\<^sub>b @ rs\<^sub>c)"}
+\]
+\noindent holds. This is indeed the case because according to the POSIX rules the
+generated bitsequence is determined by the first alternative that can match the
+string (in this case being nullable).
+\end{proof}
+\noindent
+Crucial is also the fact that derivative steps and simplification steps can be interleaved,
+which is shown by the fact that $\leadsto$ is preserved under derivatives.
 \begin{lemma}
 @{thm[mode=IfThen] rewrite_preserves_bder(1)[of "r\<^sub>1" "r\<^sub>2"]}
 \end{lemma}
-\begin{lemma}
+\begin{proof}
+By straightforward mutual induction on the definition of $\leadsto$ and $\stackrel{s}{\leadsto}$.
+The case for $LD$ holds because @{term "L (erase (bder c r\<^sub>2)) \<subseteq> L (erase (bder c r\<^sub>1))"}
+if and only if @{term "L (erase (r\<^sub>2)) \<subseteq> L (erase (r\<^sub>1))"}.
+\end{proof}
+\noindent
+Using this fact together with Lemma~\ref{lemone} allows us to prove the central lemma
+that the unsimplified
+derivative (with a string @{term s}) reduces to the simplified derivative (with the same string).
+\begin{lemma}\label{lemtwo}
 @{thm[mode=IfThen] central}
 \end{lemma}
+\begin{proof}
+By reverse induction on @{term s} generalising over @{text r}.
+\end{proof}
+\noindent
+With these lemmas in place we can finaly establish that @{term "blexer_simp"} and @{term "blexer"}
+generate the same value, and using Theorem~\ref{thmone} from the previous section that this value
+is indeed the POSIX value.
 \begin{theorem}
 @{thm[mode=IfThen] main_blexer_simp}
 \end{theorem}
-Sulzmann \& Lu apply simplification via a fixpoint operation
+\begin{proof}
+By unfolding the definitions and using Lemmas~\ref{lemtwo} and \ref{lemthree}.
-; also does not use erase to filter out duplicates.
+\end{proof}
-not direct correspondence with PDERs, because of example
+\noindent
-problem with retrieve
+This completes the correctness proof for the second POSIX lexing algorithm by Sulzmann and Lu.
+The interesting point of this algorithm is that the sizes of derivatives do not grow arbitrarily, which
-correctness
+we shall show next.
 \begin{figure}[t]
 \begin{center}
 \begin{tabular}{c}
-@{thm[mode=Axiom] bs1[of _ "r\<^sub>2"]}\qquad
+@{thm[mode=Axiom] bs1[of _ "r\<^sub>2"]}$S\ZERO{}_l$\qquad
-@{thm[mode=Axiom] bs2[of _ "r\<^sub>1"]}\qquad
+@{thm[mode=Axiom] bs2[of _ "r\<^sub>1"]}$S\ZERO{}_r$\\
-@{thm[mode=Axiom] bs3[of "bs\<^sub>1" "bs\<^sub>2"]}\\
+@{thm[mode=Axiom] bs3[of "bs\<^sub>1" "bs\<^sub>2"]}$S\ONE$\\
-@{thm[mode=Rule] bs4[of "r\<^sub>1" "r\<^sub>2" _ "r\<^sub>3"]}\qquad
+@{thm[mode=Rule] bs4[of "r\<^sub>1" "r\<^sub>2" _ "r\<^sub>3"]}SL\qquad
-@{thm[mode=Rule] bs5[of "r\<^sub>3" "r\<^sub>4" _ "r\<^sub>1"]}\\
+@{thm[mode=Rule] bs5[of "r\<^sub>3" "r\<^sub>4" _ "r\<^sub>1"]}SR\\
-@{thm[mode=Axiom] bs6}\qquad
+@{thm[mode=Axiom] bs6}$A0$\qquad
-@{thm[mode=Axiom] bs7}\\
+@{thm[mode=Axiom] bs7}$A1$\\
-@{thm[mode=Rule] bs8[of "rs\<^sub>1" "rs\<^sub>2"]}\\
+@{thm[mode=Rule] bs8[of "rs\<^sub>1" "rs\<^sub>2"]}$AL$\\
-%@ { t hm[mode=Axiom] ss1}\qquad
+@{thm[mode=Rule] ss2[of "rs\<^sub>1" "rs\<^sub>2"]}$LH$\qquad
-@{thm[mode=Rule] ss2[of "rs\<^sub>1" "rs\<^sub>2"]}\qquad
+@{thm[mode=Rule] ss3[of "r\<^sub>1" "r\<^sub>2"]}$LT$\\
-@{thm[mode=Rule] ss3[of "r\<^sub>1" "r\<^sub>2"]}\\
+@{thm[mode=Axiom] ss4}$L\ZERO$\qquad
-@{thm[mode=Axiom] ss4}\qquad
+@{thm[mode=Axiom] ss5[of "bs" "rs\<^sub>1" "rs\<^sub>2"]}$LS$\medskip\\
-@{thm[mode=Axiom] ss5[of "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\
+@{thm[mode=Rule] ss6[of "r\<^sub>2" "r\<^sub>1" "rs\<^sub>1" "rs\<^sub>2" "rs\<^sub>3"]}$LD$\\
-@{thm[mode=Rule] ss6[of "r\<^sub>2" "r\<^sub>1" "rs\<^sub>1" "rs\<^sub>2" "rs\<^sub>3"]}\\
 \end{tabular}
 \end{center}
-\caption{???}\label{SimpRewrites}
+\caption{The rewrite rules that generate simplified regular expressions
+in small steps: @{term "rrewrite r\<^sub>1 r\<^sub>2"} is for bitcoded regular
+expressions and @{term "rrewrites rs\<^sub>1 rs\<^sub>2"} for \emph{lists} of bitcoded
+regular expressions. Interesting is the $LD$ rule that allows copies of regular
+expressions be removed provided a regular expression earlier in the list can
+match the same strings.}\label{SimpRewrites}
 \end{figure}
 *}
 section {* Bound - NO *}
 section {* Conclusion *}
 text {*
+We set out in this work to implement in Isabelle/HOL the secod lexing
+algorithm by Sulzmann and Lu \cite{Sulzmann2014}. This algorithm is
+interesting because it includes an ``aggressive'' simplification
+function that keeps the sizes of derivatives finite.
+Having proved the correctness of the POSIX lexing algorithm in
+[53], which lessons have we learned? Well, we feel this is a
+perfect example where formal proofs give further insight into the
+matter at hand. Our proofs were done both done by hand and
+checked in Isabelle/HOL. The experience of doing our proofs in this
+way has been that the mechanical checking was absolutely essential:
+despite the apparent maturity, this subject area has hidden
+snares.
 %%\bibliographystyle{plain}
 \bibliography{root}
 *}

changeset 425	14c558ae0b09
parent 424	2416fdec6396
child 426	5b77220fdf01