--- a/thys2/Paper/Paper.thy Sun Feb 06 00:02:04 2022 +0000
+++ b/thys2/Paper/Paper.thy Mon Feb 07 01:11:25 2022 +0000
@@ -17,9 +17,12 @@
abbreviation
"der_syn r c \<equiv> der c r"
+abbreviation
+ "bder_syn r c \<equiv> bder c r"
notation (latex output)
der_syn ("_\\_" [79, 1000] 76) and
+ bder_syn ("_\\_" [79, 1000] 76) and
ZERO ("\<^bold>0" 81) and
ONE ("\<^bold>1" 81) and
@@ -54,10 +57,12 @@
code ("code _" [79] 74) and
intern ("_\<^latex>\<open>\\mbox{$^\\uparrow$}\<close>" [900] 80) and
erase ("_\<^latex>\<open>\\mbox{$^\\downarrow$}\<close>" [1000] 74) and
- bnullable ("nullable\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and
- bmkeps ("mkeps\<^latex>\<open>\\mbox{$_b$}\<close> _" [1000] 80) and
+ bnullable ("bnullable _" [1000] 80) and
+ bmkeps ("bmkeps _" [1000] 80) and
- srewrite ("_\<^latex>\<open>\\mbox{$\\,\\stackrel{s}{\\leadsto}$}\<close> _" [71, 71] 80)
+ srewrite ("_\<^latex>\<open>\\mbox{$\\,\\stackrel{s}{\\leadsto}$}\<close> _" [71, 71] 80) and
+ rrewrites ("_ \<^latex>\<open>\\mbox{$\\,\\leadsto^*$}\<close> _" [71, 71] 80) and
+ blexer_simp ("blexer\<^sup>+" 1000)
lemma better_retrieve:
@@ -263,7 +268,7 @@
\end{tabular}
\end{center}
- \noindent where @{text bs} stands for a bitsequences; @{text r},
+ \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"}
@@ -271,9 +276,8 @@
For bitsequences we just 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
- as part of the regular expression constructors.
- Sulzmann and Lu then define a coding
+ 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.
\begin{center}
@@ -297,8 +301,8 @@
\noindent
As can be seen, this coding is ``lossy'' in the sense that we do not
record explicitly character values and also not sequence values (for
- them we just append two bitsequences). We do, however, record the
- different alternatives for @{text Left}, respectively @{text Right}, as @{text Z} and
+ them we just append two bitsequences). However, the
+ different alternatives for @{text Left}, respectively @{text Right}, are recorded as @{text Z} and
@{text S} followed by some bitsequence. Similarly, we use @{text Z} to indicate
if there is still a value coming in the list of @{text Stars}, whereas @{text S}
indicates the end of the list. The lossiness makes the process of
@@ -404,55 +408,55 @@
bitcoded regular expressions, instead of regular expressions.
\begin{center}
- \begin{tabular}{lcl}
- $\textit{bnullable}\,(\textit{ZERO})$ & $\dn$ & $\textit{false}$ \textbf{fix}\\
+ \begin{tabular}{@ {}c@ {}c@ {}}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ $\textit{bnullable}\,(\textit{ZERO})$ & $\dn$ & $\textit{false}$\\
$\textit{bnullable}\,(\textit{ONE}\,bs)$ & $\dn$ & $\textit{true}$\\
$\textit{bnullable}\,(\textit{CHAR}\,bs\,c)$ & $\dn$ & $\textit{false}$\\
- $\textit{bnullable}\,(\textit{ALT}\,bs\,a_1\,a_2)$ & $\dn$ &
- $\textit{bnullable}\,a_1\vee \textit{bnullable}\,a_2$\\
- $\textit{bnullable}\,(\textit{SEQ}\,bs\,a_1\,a_2)$ & $\dn$ &
- $\textit{bnullable}\,a_1\wedge \textit{bnullable}\,a_2$\\
- $\textit{bnullable}\,(\textit{STAR}\,bs\,a)$ & $\dn$ &
+ $\textit{bnullable}\,(\textit{ALTs}\,bs\,\rs)$ & $\dn$ &
+ $\exists\, r \in \rs. \,\textit{bnullable}\,r$\\
+ $\textit{bnullable}\,(\textit{SEQ}\,bs\,r_1\,r_2)$ & $\dn$ &
+ $\textit{bnullable}\,r_1\wedge \textit{bnullable}\,r_2$\\
+ $\textit{bnullable}\,(\textit{STAR}\,bs\,r)$ & $\dn$ &
$\textit{true}$
- \end{tabular}
- \end{center}
-
- \begin{center}
- \begin{tabular}{lcl}
- $\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$ \textbf{fix}\\
- $\textit{bmkeps}\,(\textit{ALT}\,bs\,a_1\,a_2)$ & $\dn$ &
- $\textit{if}\;\textit{bnullable}\,a_1$\\
- & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a_1$\\
- & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,a_2$\\
- $\textit{bmkeps}\,(\textit{SEQ}\,bs\,a_1\,a_2)$ & $\dn$ &
- $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
- $\textit{bmkeps}\,(\textit{STAR}\,bs\,a)$ & $\dn$ &
+ \end{tabular}
+ &
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ $\textit{bmkeps}\,(\textit{ONE}\,bs)$ & $\dn$ & $bs$\\
+ $\textit{bmkeps}\,(\textit{ALTs}\,bs\,r\!::\!\rs)$ & $\dn$ &
+ $\textit{if}\;\textit{bnullable}\,r$\\
+ & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,r$\\
+ & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,\rs$\\
+ $\textit{bmkeps}\,(\textit{SEQ}\,bs\,r_1\,r_2)$ & $\dn$ &\\
+ \multicolumn{3}{r}{$bs \,@\,\textit{bmkeps}\,r_1\,@\, \textit{bmkeps}\,r_2$}\\
+ $\textit{bmkeps}\,(\textit{STAR}\,bs\,r)$ & $\dn$ &
$bs \,@\, [\S]$
- \end{tabular}
+ \end{tabular}
+ \end{tabular}
\end{center}
\noindent
The key function in the bitcoded algorithm is the derivative of an
- annotated regular expression. This derivative calculates the
- derivative but at the same time also the incremental part that
- contributes to constructing a value.
+ bitcoded regular expression. This derivative calculates the
+ derivative but at the same time also the incremental part of bitsequences
+ that contribute to constructing a POSIX value.
\begin{center}
\begin{tabular}{@ {}lcl@ {}}
- $(\textit{ZERO})\backslash c$ & $\dn$ & $\textit{ZERO}$ \textbf{fix}\\
+ $(\textit{ZERO})\backslash c$ & $\dn$ & $\textit{ZERO}$ \\
$(\textit{ONE}\;bs)\backslash c$ & $\dn$ & $\textit{ZERO}$\\
$(\textit{CHAR}\;bs\,d)\backslash c$ & $\dn$ &
$\textit{if}\;c=d\; \;\textit{then}\;
\textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\
- $(\textit{ALT}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
- $\textit{ALT}\,bs\,(a_1\backslash c)\,(a_2\backslash c)$\\
- $(\textit{SEQ}\;bs\,a_1\,a_2)\backslash c$ & $\dn$ &
- $\textit{if}\;\textit{bnullable}\,a_1$\\
- & &$\textit{then}\;\textit{ALT}\,bs\,(\textit{SEQ}\,[]\,(a_1\backslash c)\,a_2)$\\
- & &$\phantom{\textit{then}\;\textit{ALT}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\backslash c))$\\
- & &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\backslash c)\,a_2$\\
- $(\textit{STAR}\,bs\,a)\backslash c$ & $\dn$ &
+ $(\textit{ALTs}\;bs\,\rs)\backslash c$ & $\dn$ &
+ $\textit{ALTs}\,bs\,(\mathit{map}\,(\_\backslash c)\,\rs)$\\
+ $(\textit{SEQ}\;bs\,r_1\,r_2)\backslash c$ & $\dn$ &
+ $\textit{if}\;\textit{bnullable}\,r_1$\\
+ & &$\textit{then}\;\textit{ALT}\,bs\,(\textit{SEQ}\,[]\,(r_1\backslash c)\,r_2)$\\
+ & &$\phantom{\textit{then}\;\textit{ALT}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,r_1)\,(r_2\backslash c))$\\
+ & &$\textit{else}\;\textit{SEQ}\,bs\,(r_1\backslash c)\,r_2$\\
+ $(\textit{STAR}\,bs\,r)\backslash c$ & $\dn$ &
$\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\backslash c))\,
(\textit{STAR}\,[]\,r)$
\end{tabular}
@@ -460,66 +464,32 @@
\noindent
- This function can also be extended to strings, written $a\backslash s$,
+ This function can also be extended to strings, written $r\backslash s$,
just like the standard derivative. We omit the details. Finally we
- can define Sulzmann and Lu's bitcoded lexer, which we call \textit{blexer}:
+ can define Sulzmann and Lu's bitcoded lexer, which we call \textit{blexer}:
+
+ \begin{center}
+\begin{tabular}{lcl}
+ $\textit{blexer}\;r\,s$ & $\dn$ &
+ $\textit{let}\;r_{der} = (r^\uparrow)\backslash 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
This bitcoded lexer first internalises the regular expression $r$ and then
-builds the annotated derivative according to $s$. If the derivative is
-nullable, then it extracts the bitcoded value using the
-$\textit{bmkeps}$ function. Finally it decodes the bitcoded value. If
+builds the bitcoded derivative according to $s$. If the derivative is
+(b)nullable the string is in the language of $r$ and it extracts the bitsequence using the
+$\textit{bmkeps}$ function. Finally it decodes the bitsequence into a value. If
the derivative is \emph{not} nullable, then $\textit{None}$ is
-returned. The task is to show that this way of calculating a value
+returned. We can show that this way of calculating a value
generates the same result as with \textit{lexer}.
-Before we can proceed we need to define a function, called
-\textit{retrieve}, which Sulzmann and Lu introduced for the proof.
-
-\textbf{fix}
-
-\noindent
-The idea behind this function is to retrieve a possibly partial
-bitcode from an annotated regular expression, where the retrieval is
-guided by a value. For example if the value is $\Left$ then we
-descend into the left-hand side of an alternative (annotated) regular
-expression in order to assemble the bitcode. Similarly for
-$\Right$. The property we can show is that for a given $v$ and $r$
-with $\vdash v : r$, the retrieved bitsequence from the internalised
-regular expression is equal to the bitcoded version of $v$.
-
-\begin{lemma}\label{retrievecode}
-If $\vdash v : r$ then $\textit{code}\, v = \textit{retrieve}\,(r^\uparrow)\,v$.
-\end{lemma}
-
-*}
+Before we can proceed we need to define a helper function, called
+\textit{retrieve}, which Sulzmann and Lu introduced for the correctness proof.
-text {*
- There is also a corresponding decoding function that takes a bitsequence
- and generates back a value. However, since the bitsequences are a ``lossy''
- coding (@{term Seq}s are not coded) the decoding function depends also
- on a regular expression in order to decode values.
-
-
-
-
- The idea of the bitcodes is to annotate them to regular expressions and generate values
- incrementally. The bitcodes can be read off from the @{text breg} and then decoded into a value.
-
- \begin{center}
- \begin{tabular}{lcl}
- @{term breg} & $::=$ & @{term "AZERO"}\\
- & $\mid$ & @{term "AONE bs"}\\
- & $\mid$ & @{term "ACHAR bs c"}\\
- & $\mid$ & @{term "AALTs bs rs"}\\
- & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\
- & $\mid$ & @{term "ASTAR bs r"}
- \end{tabular}
- \end{center}
-
-
-
- \begin{center}
+\begin{center}
\begin{tabular}{lcl}
@{thm (lhs) retrieve.simps(1)} & $\dn$ & @{thm (rhs) retrieve.simps(1)}\\
@{thm (lhs) retrieve.simps(2)} & $\dn$ & @{thm (rhs) retrieve.simps(2)}\\
@@ -533,22 +503,171 @@
\end{tabular}
\end{center}
+\noindent
+The idea behind this function is to retrieve a possibly partial
+bitcode from a bitcoded regular expression, where the retrieval is
+guided by a value. For example if the value is $\Left$ then we
+descend into the left-hand side of an alternative in order to
+assemble the bitcode. Similarly for
+$\Right$. The property we can show is that for a given $v$ and $r$
+with $\vdash v : r$, the retrieved bitsequence from the internalised
+regular expression is equal to the bitcoded version of $v$.
- \begin{theorem}
- @{thm blexer_correctness}
- \end{theorem}
+\begin{lemma}\label{retrievecode}
+If $\vdash v : r$ then $\textit{code}\, v = \textit{retrieve}\,(r^\uparrow)\,v$.
+\end{lemma}
+
+\noindent
+We also need some auxiliary facts about how the bitcoded operations
+relate to the ``standard'' operations on regular expressions. For
+example if we build a bitcoded derivative and erase the result, this
+is the same as if we first erase the bitcoded regular expression and
+then perform the ``standard'' derivative operation.
+
+\begin{lemma}\label{bnullable}\mbox{}\smallskip\\
+ \begin{tabular}{ll}
+\textit{(1)} & $(a\backslash s)^\downarrow = (a^\downarrow)\backslash s$\\
+\textit{(2)} & $\textit{bnullable}(a)$ iff $\textit{nullable}(a^\downarrow)$\\
+\textit{(3)} & $\textit{bmkeps}(a) = \textit{retrieve}\,a\,(\textit{mkeps}\,(a^\downarrow))$ provided $\textit{nullable}(a^\downarrow)$.
+\end{tabular}
+\end{lemma}
+
+\begin{proof}
+ All properties are by induction on annotated regular expressions. There are no
+ interesting cases.
+\end{proof}
+
+\noindent
+This brings us to our main lemma in this section: if we build a
+derivative, say $r\backslash s$ and have a value, say $v$, inhabited
+by this derivative, then we can produce the result $\lexer$ generates
+by applying this value to the stacked-up injection functions
+$\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.
+
+\begin{lemma}[Main Lemma]\label{mainlemma}\it
+If $\vdash v : r\backslash s$ then
+\[\textit{Some}\,(\textit{flex}\,r\,\textit{id}\,s\,v) =
+ \textit{decode}(\textit{retrieve}\,(r^\uparrow \backslash s)\,v)\,r\]
+\end{lemma}
+
+\begin{proof}
+ This can be proved by induction on $s$ and generalising over
+ $v$. The interesting point is that we need to prove this in the
+ reverse direction for $s$. This means instead of cases $[]$ and
+ $c\!::\!s$, we have cases $[]$ and $s\,@\,[c]$ where we unravel the
+ string from the back.\footnote{Isabelle/HOL provides an induction principle
+ for this way of performing the induction.}
+
+ The case for $[]$ is routine using Lemmas~\ref{codedecode}
+ and~\ref{retrievecode}. In the case $s\,@\,[c]$, we can infer from
+ the assumption that $\vdash v : (r\backslash s)\backslash c$
+ holds. Hence by Lemma~\ref{Posix2} we know that
+ (*) $\vdash \inj\,(r\backslash s)\,c\,v : r\backslash s$ holds too.
+ By definition of $\textit{flex}$ we can unfold the left-hand side
+ to be
+ \[
+ \textit{Some}\,(\textit{flex}\;r\,\textit{id}\,(s\,@\,[c])\,v) =
+ \textit{Some}\,(\textit{flex}\;r\,\textit{id}\,s\,(\inj\,(r\backslash s)\,c\,v))
+ \]
+
+ \noindent
+ By induction hypothesis and (*) we can rewrite the right-hand side to
+
+ \[
+ \textit{decode}\,(\textit{retrieve}\,(r^\uparrow\backslash s)\;
+ (\inj\,(r\backslash s)\,c\,\,v))\,r
+ \]
+
+ \noindent
+ which is equal to
+ $\textit{decode}\,(\textit{retrieve}\, (r^\uparrow\backslash
+ (s\,@\,[c]))\,v)\,r$ as required. The last rewrite step is possible
+ because we generalised over $v$ in our induction.
+\end{proof}
+
+\noindent
+With this lemma in place, we can prove the correctness of \textit{blexer} such
+that it produces the same result as \textit{lexer}.
- bitcoded regexes / decoding / bmkeps
- gets rid of the second phase (only single phase)
- correctness
+\begin{theorem}
+$\textit{lexer}\,r\,s = \textit{blexer}\,r\,s$
+\end{theorem}
+
+\begin{proof}
+ We can first expand both sides using Lemma~\ref{flex} and the
+ definition of \textit{blexer}. This gives us two
+ \textit{if}-statements, which we need to show to be equal. By
+ Lemma~\ref{bnullable}\textit{(2)} we know the \textit{if}-tests coincide:
+ \[
+ \textit{bnullable}(r^\uparrow\backslash s) \;\textit{iff}\;
+ \nullable(r\backslash s)
+ \]
+
+ \noindent
+ For the \textit{if}-branch suppose $r_d \dn r^\uparrow\backslash s$ and
+ $d \dn r\backslash s$. We have (*) $\nullable\,d$. We can then show
+ by Lemma~\ref{bnullable}\textit{(3)} that
+ %
+ \[
+ \textit{decode}(\textit{bmkeps}\,r_d)\,r =
+ \textit{decode}(\textit{retrieve}\,a\,(\textit{mkeps}\,d))\,r
+ \]
+
+ \noindent
+ where the right-hand side is equal to
+ $\textit{Some}\,(\textit{flex}\,r\,\textit{id}\,s\,(\textit{mkeps}\,
+ d))$ by Lemma~\ref{mainlemma} (we know
+ $\vdash \textit{mkeps}\,d : d$ by (*)). This shows the
+ \textit{if}-branches return the same value. In the
+ \textit{else}-branches both \textit{lexer} and \textit{blexer} return
+ \textit{None}. Therefore we can conclude the proof.
+\end{proof}
+
+\noindent
+This establishes that the bitcoded algorithm by Sulzmann
+and Lu without simplification produces correct results. This was
+only conjectured in their paper \cite{Sulzmann2014}. The next step
+is to add simplifications.
+
*}
section {* Simplification *}
text {*
- Sulzmann \& Lu apply simplification via a fixpoint operation; also does not use erase to filter out duplicates.
+
+ \begin{lemma}
+ @{thm[mode=IfThen] bnullable0(1)[of "r\<^sub>1" "r\<^sub>2"]}
+ \end{lemma}
+
+
+ \begin{lemma}
+ @{thm[mode=IfThen] rewrite_bmkeps_aux(1)[of "r\<^sub>1" "r\<^sub>2"]}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm[mode=IfThen] rewrites_to_bsimp}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm[mode=IfThen] rewrite_preserves_bder(1)[of "r\<^sub>1" "r\<^sub>2"]}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm[mode=IfThen] central}
+ \end{lemma}
+
+ \begin{theorem}
+ @{thm[mode=IfThen] main_blexer_simp}
+ \end{theorem}
+
+ Sulzmann \& Lu apply simplification via a fixpoint operation
+
+ ; also does not use erase to filter out duplicates.
not direct correspondence with PDERs, because of example
problem with retrieve