22   val.Void ("'(')" 78) and

    22   val.Void ("'(')" 79) and

    23   val.Char ("Char _" [1000] 78) and

    23   val.Char ("Char _" [1000] 79) and

    29   flat ("|_|" [70] 73) and

    29   flat ("|_|" [75] 73) and

    31   injval ("inj _ _ _" [1000,77,1000] 77) and 

    31   injval ("inj _ _ _" [78,77,78] 77) and 

    33   length ("len _" [78] 73) 

    33   length ("len _" [78] 73) and

    34 

    35   Prf ("\<triangleright> _ : _" [75,75] 75) and  

    36   PMatch ("_ : _ \<rightarrow> _" [75,75,75] 75)

    62 that appears to be the value associated with POSIX lexing

    66 that appears to be the value associated with POSIX matching

    89 If a regular expression matches a string, then in general there is more

    93 If a regular expression matches a string, then in general there is more than

    90 than one way of how the string is matched. There are two commonly used

    94 one way of how the string is matched. There are two commonly used

    93 matching~\cite{Kuklewicz,Sulzmann2014}. For example consider the string

    97 matching~\cite{Kuklewicz,Sulzmann2014,Vansummeren2006}. For example consider

    94 @{term xy} and the regular expression \mbox{@{term "STAR (ALT (ALT x y)

    98 the string @{term xy} and the regular expression \mbox{@{term "STAR (ALT

    95 xy)"}}. Either the string can be matched in two `iterations' by the single

    99 (ALT x y) xy)"}}. Either the string can be matched in two `iterations' by

    96 letter-regular expressions @{term x} and @{term y}, or directly in one

   100 the single letter-regular expressions @{term x} and @{term y}, or directly

    97 iteration by @{term xy}. The first case corresponds to GREEDY matching,

   101 in one iteration by @{term xy}. The first case corresponds to GREEDY

    98 which first matches with the left-most symbol and only matches the next

   102 matching, which first matches with the left-most symbol and only matches the

    99 symbol in case of a mismatch (this is greedy in the sense of preferring

   103 next symbol in case of a mismatch (this is greedy in the sense of preferring

   123 \noindent Consider for example @{text "r\<^bsub>key\<^esub>"} recognising

   127 \noindent Consider for example @{text "r\<^bsub>key\<^esub>"} recognising keywords such as

   124 keywords such as @{text "if"}, @{text "then"} and so on; and @{text

   128 @{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"} recognising

   125 "r\<^bsub>id\<^esub>"} recognising identifiers (a single character followed

   129 identifiers (a single character followed by characters or numbers). Then we

   126 by characters or numbers). Then we can form the regular expression @{text

   130 can form the regular expression @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and use POSIX

   127 "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and use POSIX

   130 not a keyword followed by identifier. In the second case we obtain by rule

   133 not a keyword followed by an identifier. In the second case we obtain by rule

   131 priority a keyword token, not an identifier token---even if @{text

   134 priority a keyword token, not an identifier token---even if @{text "r\<^bsub>id\<^esub>"}

   132 "r\<^bsub>id\<^esub>"} matches also.\bigskip

   135 matches also.\bigskip

   133 

   136 

   134 \noindent\textcolor{green}{Not Done Yet}

   137 \noindent {\bf Contributions:} We have implemented in Isabelle/HOL the

   135 

   138 derivative-based regular expression matching algorithm as described by

   136 

   139 Sulzmann and Lu \cite{Sulzmann2014}. We have proved the correctness of this

   137 \medskip\noindent

   140 algorithms according to our specification what a POSIX value is. The

   138 {\bf Contributions:}

   141 informal correctness proof given in \cite{Sulzmann2014} is in final

   139 

   142 form\footnote{} and to us contains unfillable gaps. Our specification of a

   140 Derivatives as calculated by Brzozowski's method are usually more complex

   143 POSIX value consists of a simple inductive definition that given a string

   141 regular expressions than the initial one; various optimisations are

   144 and a regular expression uniquely determines this value. Derivatives as

   142 possible, such as the simplifications of @{term "ALT ZERO r"}, @{term "ALT r

   145 calculated by Brzozowski's method are usually more complex regular

   143 ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to @{term r}. One of the

   146 expressions than the initial one; various optimisations are possible, such

   144 advantages of having a simple specification and correctness proof is that

   147 as the simplifications of @{term "ALT ZERO r"}, @{term "ALT r ZERO"}, @{term

   145 the latter can be refined to allow for such optimisations and simple

   148 "SEQ ONE r"} and @{term "SEQ r ONE"} to @{term r}. One of the advantages of

   146 correctness proof.

   149 having a simple specification and correctness proof is that the latter can

   147 

   150 be refined to allow for such optimisations and simple correctness proof.

   148 An extended version of \cite{Sulzmann2014} is available at the website

   151 

   149 of its first author; this includes some ``proofs'', claimed in

   152 An extended version of \cite{Sulzmann2014} is available at the website of

   153 its first author; this includes some ``proofs'', claimed in

   151 final form, we make no comment thereon, preferring to give general

   155 final form, we make no comment thereon, preferring to give general reasons

   152 reasons for our belief that the approach of \cite{Sulzmann2014} is

   156 for our belief that the approach of \cite{Sulzmann2014} is problematic

   153 problematic rather than to discuss details of unpublished work.

   157 rather than to discuss details of unpublished work.

   154 

   163 bracket notation for strings; for example a string consisting of just a

   166 bracket notation for lists also for strings; for example a string consisting

   164 single character is written @{term "[c]"}. By using the type @{type char}

   167 of just a single character @{term c} is written @{term "[c]"}. By using the

   165 for characters we have a supply of finitely many characters roughly

   168 type @{type char} for characters we have a supply of finitely many

   166 corresponding to the ASCII character set. Regular expressions are defined as

   169 characters roughly corresponding to the ASCII character set. Regular

   167 usual as the following inductive datatype:

   170 expressions are defined as usual as the following inductive datatype:

   179   \noindent where @{const ZERO} stands for the regular expression that

   182   \noindent where @{const ZERO} stands for the regular expression that does

   180   does not match any string and @{const ONE} for the regular

   183   not match any string, @{const ONE} for the regular expression that matches

   181   expression that matches only the empty string. The language of a regular expression

   184   only the empty string and @{term c} for matching a character literal. The

   182   is again defined routinely by the recursive function @{term L} with the

   185   language of a regular expression is again defined as usual by the

   183   clauses:

   186   recursive function @{term L} with the clauses:

   198   use the star-notation for regular expressions and also for languages (in

   201   use the star-notation for regular expressions and languages (in the last

   199   the last clause). The star for languages is defined inductively as usual

   202   clause above). The star on languages is defined inductively by two

   200   by two clauses for the empty string being in the star of a language and if

   203   clauses: @{text "(i)"} for the empty string being in the star of a

   201   @{term "s\<^sub>1"} is in a language and @{term "s\<^sub>2"} in the star of this

   204   language and @{text "(ii)"} if @{term "s\<^sub>1"} is in a language and @{term

   202   language, then also @{term "s\<^sub>1 @ s\<^sub>2"} is in the star of this language.

   205   "s\<^sub>2"} in the star of this language, then also @{term "s\<^sub>1 @ s\<^sub>2"} is in

   203   

   206   the star of this language. It will also be convenient to use the following

   204   \emph{Semantic derivatives} of sets of strings are defined as

   207   notion of a \emph{semantic derivative} (or left quotient) of a language,

   208   say @{text A}, defined as:

   212   

   216   \noindent 

   213 

   217   For semantic derivatives we have the following equations (for example

   214   \noindent

   218   \cite{Krauss2011}):

   215   The nullable function

   219 

   220   \begin{equation}

   221   \begin{array}{lcl}

   222   @{thm (lhs) Der_null}  & \dn & @{thm (rhs) Der_null}\\

   223   \end{array}

   224   \end{equation}

   225 

   226 

   227   \noindent \emph{\Brz's derivatives} of regular expressions

   228   \cite{Brzozowski1964} can be easily defined by two recursive functions:

   229   the first is from regular expressions to booleans (implementing a test

   230   when a regular expression can match the empty string), and the second

   231   takes a regular expression and a character to a (derivative) regular

   232   expression:

   224   @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\\

   241   @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\

   225   \end{tabular}

   226   \end{center}

   227 

   228   \noindent

   229   The derivative function for characters and strings

   230 

   231   \begin{center}

   232   \begin{tabular}{lcp{8cm}}

   242   It is a relatively easy exercise to prove that

   251   \noindent

   243 

   252   Given the equations in ???, 

   244   \begin{center}

   253   it is a relatively easy exercise in mechanical reasoning to establish that

   245   \begin{tabular}{l}

   254 

   246   @{thm[mode=IfThen] nullable_correctness}\\

   255   \begin{proposition} 

   247   @{thm[mode=IfThen] der_correctness}\\

   256   \begin{tabular}{ll}

   248   \end{tabular}

   257   @{text "(1)"} & @{thm (lhs) nullable_correctness} if and only if

   249   \end{center}

   258   @{thm (rhs) nullable_correctness} \\ 

   259   @{text "(2)"} & @{thm[mode=IfThen] der_correctness}

   260   \end{tabular}

   261   \end{proposition}

   262 

   263   \noindent With this in place it is also very routine to prove that the

   264   regular expression matcher defined as

   265 

   266   \begin{center}

   267 

   268   \end{center}

   269 

   270   While the matcher above calculates a provably correct a YES/NO answer for

   271   whether a regular expression matches a string, the novel idea of Sulzmann

   272   and Lu \cite{Sulzmann2014} is to append another phase to calculate a

   273   value.

   274 

   256 The clever idea in \cite{Sulzmann2014} is to define a function on values that mirrors

   281 The clever idea in \cite{Sulzmann2014} is to introduce values for encoding

   257 (but inverts) the construction of the derivative on regular expressions. We

   282 \emph{how} a regular expression matches a string and then define a function

   258 begin with the case of a nullable regular expression: from the nullability

   283 on values that mirrors (but inverts) the construction of the derivative on

   259 we need to construct a value that witnesses the nullability. This is as

   284 regular expressions. Values are defined as the inductive datatype

   260 follows. The @{const mkeps} function (from \cite{Sulzmann2014}) is a partial (but

   285 

   261 unambiguous) function from regular expressions to values, total on exactly

   286   \begin{center}

   262 the set of nullable regular expressions. 

   287   @{text "v :="}

   288   @{const "Void"} $\mid$

   289   @{term "val.Char c"} $\mid$

   290   @{term "Left v"} $\mid$

   291   @{term "Right v"} $\mid$

   292   @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ 

   293   @{term "Stars vs"} 

   294   \end{center}  

   295 

   296 The inhabitation relation:

   297 

   298   \begin{center}

   299   \begin{tabular}{c}

   300   @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\medskip\\ 

   301   @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad 

   302   @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\medskip\\

   303   @{thm[mode=Axiom] Prf.intros(4)} \qquad 

   304   @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\medskip\\

   305   @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad 

   306   @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}\medskip\\

   307   \end{tabular}

   308   \end{center}

   309 

   310 

   311 Note that no values are associated with the regular expression $Zero$, and

   312 that the only value associated with the regular expression $One$ is $Void$,

   313 pronounced (if one must) as {\em ``Void''}. We use $\in$ for the usual

   314 membership relation from set theory and take $[]$ as the standard name for

   315 the empty string (rather than, as in \cite{Sulzmann2014}, the regular

   316 expression that we call $One$).

   317 

   318 We begin with the case of a nullable regular expression: from

   319 the nullability we need to construct a value that witnesses the nullability.

   320 The @{const mkeps} function (from \cite{Sulzmann2014})

   321 is a partial (but unambiguous) function from regular expressions to values,

   322 total on exactly the set of nullable regular expressions.

   326   \begin{center}

   386   

   327   @{text "v :="}

   328   @{const "Void"} $\mid$

   329   @{term "val.Char c"} $\mid$

   330   @{term "Left v"} $\mid$

   331   @{term "Right v"} $\mid$

   332   @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ 

   333   @{term "Stars vs"} 

   334   \end{center}