# HG changeset patch # User Christian Urban # Date 1457156511 0 # Node ID 8b41d01b5e5d8e3f945f333890b0a00ce429652f # Parent 90fe1a1d7d0e0a50d5330bb62f97c7d390555cc7 updated diff -r 90fe1a1d7d0e -r 8b41d01b5e5d Literature/berrysethi.pdf Binary file Literature/berrysethi.pdf has changed diff -r 90fe1a1d7d0e -r 8b41d01b5e5d thys/Paper/Paper.thy --- a/thys/Paper/Paper.thy Sat Mar 05 04:01:10 2016 +0000 +++ b/thys/Paper/Paper.thy Sat Mar 05 05:41:51 2016 +0000 @@ -8,6 +8,9 @@ abbreviation "der_syn r c \ der c r" +abbreviation + "ders_syn r s \ ders s r" + notation (latex output) If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [78,77] 73) and @@ -25,7 +28,8 @@ val.Right ("Right _" [1000] 78) and L ("L'(_')" [10] 78) and - der_syn ("_\\_" [79, 1000] 76) and + der_syn ("_\\_" [79, 1000] 76) and + ders_syn ("_\\_" [79, 1000] 76) and flat ("|_|" [75] 73) and Sequ ("_ @ _" [78,77] 63) and injval ("inj _ _ _" [78,77,78] 77) and @@ -35,6 +39,10 @@ Prf ("\ _ : _" [75,75] 75) and PMatch ("_ : _ \ _" [75,75,75] 75) (* and ValOrd ("_ \\<^bsub>_\<^esub> _" [78,77,77] 73) *) + +definition + "match r s \ nullable (ders s r)" + (*>*) section {* Introduction *} @@ -217,9 +225,14 @@ For semantic derivatives we have the following equations (for example \cite{Krauss2011}): - \begin{equation} + \begin{equation}\label{SemDer} \begin{array}{lcl} @{thm (lhs) Der_null} & \dn & @{thm (rhs) Der_null}\\ + @{thm (lhs) Der_empty} & \dn & @{thm (rhs) Der_empty}\\ + @{thm (lhs) Der_char} & \dn & @{thm (rhs) Der_char}\\ + @{thm (lhs) Der_union} & \dn & @{thm (rhs) Der_union}\\ + @{thm (lhs) Der_Sequ} & \dn & @{thm (rhs) Der_Sequ}\\ + @{thm (lhs) Der_star} & \dn & @{thm (rhs) Der_star} \end{array} \end{equation} @@ -247,12 +260,21 @@ @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)} \end{tabular} \end{center} - + \noindent - Given the equations in ???, - it is a relatively easy exercise in mechanical reasoning to establish that + We may extend this definition to give derivatives w.r.t.~strings: - \begin{proposition} + \begin{center} + \begin{tabular}{lcl} + @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\ + @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\ + \end{tabular} + \end{center} + + \noindent Given the equations in \eqref{SemDer}, it is a relatively easy + exercise in mechanical reasoning to establish that + + \begin{proposition}\mbox{}\\ \begin{tabular}{ll} @{text "(1)"} & @{thm (lhs) nullable_correctness} if and only if @{thm (rhs) nullable_correctness} \\ @@ -264,13 +286,14 @@ regular expression matcher defined as \begin{center} - + @{thm match_def} \end{center} - While the matcher above calculates a provably correct a YES/NO answer for + \noindent gives a positive answer if and only if @{term "s \ L r"}. While + the matcher above calculates a provably correct a YES/NO answer for whether a regular expression matches a string, the novel idea of Sulzmann and Lu \cite{Sulzmann2014} is to append another phase to calculate a - value. + value. We will explain the details next. *} @@ -293,7 +316,24 @@ @{term "Stars vs"} \end{center} -The inhabitation relation: + \noindent where we use @{term vs} standing for a list of values. The string + underlying a values can be calculated by the @{const flat} function, written + @{term "flat DUMMY"} and defined as: + + \begin{center} + \begin{tabular}{lcl} + @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\ + @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\ + @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\ + @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\ + @{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ + @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\ + @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\ + \end{tabular} + \end{center} + + \noindent Sulzmann and Lu also define inductively an inhabitation relation + that associates values to regular expressions: \begin{center} \begin{tabular}{c} @@ -307,19 +347,67 @@ \end{tabular} \end{center} + \noindent Note that no values are associated with the regular expression + @{term ZERO}, and that the only value associated with the regular + expression @{term ONE} is @{term Void}, pronounced (if one must) as {\em + ``Void''}. It is routine to stablish how values `inhabitated' by a regular + expression correspond to the language of a regular expression, namely -Note that no values are associated with the regular expression $Zero$, and -that the only value associated with the regular expression $One$ is $Void$, -pronounced (if one must) as {\em ``Void''}. We use $\in$ for the usual -membership relation from set theory and take $[]$ as the standard name for -the empty string (rather than, as in \cite{Sulzmann2014}, the regular -expression that we call $One$). + \begin{proposition} + @{thm L_flat_Prf} + \end{proposition} + + Graphically the algorithm by Sulzmann \& Lu can be illustrated by the + picture in Figure~\ref{Sulz} where the path from the left to the right + involving $der/nullable$ is the first phase of the algorithm and + $mkeps/inj$, the path from right to left, the second phase. This picture + shows the steps required when a regular expression, say $r_1$, matches the + string $abc$. We first build the three derivatives (according to $a$, $b$ + and $c$). We then use $nullable$ to find out whether the resulting regular + expression can match the empty string. If yes, we call the function + $mkeps$. -We begin with the case of a nullable regular expression: from -the nullability we need to construct a value that witnesses the nullability. -The @{const mkeps} function (from \cite{Sulzmann2014}) -is a partial (but unambiguous) function from regular expressions to values, -total on exactly the set of nullable regular expressions. +\begin{figure}[t] +\begin{center} +\begin{tikzpicture}[scale=2,node distance=1.2cm, + every node/.style={minimum size=7mm}] +\node (r1) {@{term "r\<^sub>1"}}; +\node (r2) [right=of r1]{@{term "r\<^sub>2"}}; +\draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}}; +\node (r3) [right=of r2]{@{term "r\<^sub>3"}}; +\draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}}; +\node (r4) [right=of r3]{@{term "r\<^sub>4"}}; +\draw[->,line width=1mm](r3)--(r4) node[above,midway] {@{term "der c DUMMY"}}; +\draw (r4) node[anchor=west] {\;\raisebox{3mm}{@{term nullable}}}; +\node (v4) [below=of r4]{@{term "v\<^sub>4"}}; +\draw[->,line width=1mm](r4) -- (v4); +\node (v3) [left=of v4] {@{term "v\<^sub>3"}}; +\draw[->,line width=1mm](v4)--(v3) node[below,midway] {@{term "inj c"}}; +\node (v2) [left=of v3]{@{term "v\<^sub>2"}}; +\draw[->,line width=1mm](v3)--(v2) node[below,midway] {@{term "inj b"}}; +\node (v1) [left=of v2] {@{term "v\<^sub>1"}}; +\draw[->,line width=1mm](v2)--(v1) node[below,midway] {@{term "inj a"}}; +\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}}; +\end{tikzpicture} +\end{center} +\caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014} +analysing the string @{term "[a,b,c]"}. The first phase (the arrows from +left to right) is \Brz's matcher building succesive derivatives. If at the +last regular expression is @{term nullable}, then functions of the +second phase are called: first @{term mkeps} calculates a value witnessing +how the empty string has been recognised by @{term "r\<^sub>4"}. After +that the function @{term inj} `injects back' the characters of the string into +the values (the arrows from right to left). +\label{Sulz}} +\end{figure} + + NOT DONE YET + + We begin with the case of a nullable regular expression: from the + nullability we need to construct a value that witnesses the nullability. + The @{const mkeps} function (from \cite{Sulzmann2014}) is a partial (but + unambiguous) function from regular expressions to values, total on exactly + the set of nullable regular expressions. \begin{center} \begin{tabular}{lcl} @@ -387,20 +475,7 @@ - \noindent - The @{const flat} function for values - - \begin{center} - \begin{tabular}{lcl} - @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\ - @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\ - @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\ - @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\ - @{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ - @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\ - @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\ - \end{tabular} - \end{center} + \noindent The @{const mkeps} function diff -r 90fe1a1d7d0e -r 8b41d01b5e5d thys/Paper/document/root.tex --- a/thys/Paper/document/root.tex Sat Mar 05 04:01:10 2016 +0000 +++ b/thys/Paper/document/root.tex Sat Mar 05 05:41:51 2016 +0000 @@ -7,6 +7,7 @@ \usepackage{mathpartir} \usepackage{tikz} \usepackage{pgf} +\usetikzlibrary{positioning} \usepackage{pdfsetup} \usepackage{ot1patch} \usepackage{stmaryrd} diff -r 90fe1a1d7d0e -r 8b41d01b5e5d thys/paper.pdf Binary file thys/paper.pdf has changed