(*<*)+
−
theory Paper+
−
imports +
−
   "../ReStar"+
−
   "../Simplifying" +
−
   "../Sulzmann" +
−
   "~~/src/HOL/Library/LaTeXsugar"+
−
begin+
−
+
−
declare [[show_question_marks = false]]+
−
+
−
abbreviation +
−
 "der_syn r c \<equiv> der c r"+
−
+
−
abbreviation +
−
 "ders_syn r s \<equiv> 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{$\,$}>_" [75,73] 73) and  +
−
+
−
  ZERO ("\<^bold>0" 78) and +
−
  ONE ("\<^bold>1" 78) and +
−
  CHAR ("_" [1000] 80) and+
−
  ALT ("_ + _" [77,77] 78) and+
−
  SEQ ("_ \<cdot> _" [77,77] 78) and+
−
  STAR ("_\<^sup>\<star>" [1000] 78) and+
−
  +
−
  val.Void ("'(')" 1000) and+
−
  val.Char ("Char _" [1000] 78) and+
−
  val.Left ("Left _" [79] 78) and+
−
  val.Right ("Right _" [1000] 78) and+
−
  val.Seq ("Seq _ _" [79,79] 78) and+
−
  val.Stars ("Stars _" [79] 78) and+
−
+
−
  L ("L'(_')" [10] 78) and+
−
  der_syn ("_\\_" [79, 1000] 76) and  +
−
  ders_syn ("_\\_" [79, 1000] 76) and+
−
  flat ("|_|" [75] 74) and+
−
  Sequ ("_ @ _" [78,77] 63) and+
−
  injval ("inj _ _ _" [79,77,79] 76) and +
−
  mkeps ("mkeps _" [79] 76) and +
−
  length ("len _" [73] 73) and+
−
 +
−
  Prf ("_ : _" [75,75] 75) and  +
−
  Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and+
−
 +
−
  lexer ("lexer _ _" [78,78] 77) and +
−
  F_RIGHT ("F\<^bsub>Right\<^esub> _") and+
−
  F_LEFT ("F\<^bsub>Left\<^esub> _") and  +
−
  F_ALT ("F\<^bsub>Alt\<^esub> _ _") and+
−
  F_SEQ1 ("F\<^bsub>Seq1\<^esub> _ _") and+
−
  F_SEQ2 ("F\<^bsub>Seq2\<^esub> _ _") and+
−
  F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and+
−
  simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and+
−
  simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and+
−
  slexer ("lexer\<^sup>+" 1000) and+
−
+
−
  ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and+
−
  ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)+
−
+
−
definition +
−
  "match r s \<equiv> nullable (ders s r)"+
−
+
−
(*+
−
comments not implemented+
−
+
−
p9. The condtion "not exists s3 s4..." appears often enough (in particular in+
−
the proof of Lemma 3) to warrant a definition.+
−
+
−
p10. (proof Lemma 3) : separating the cases with description/itemize would greatly+
−
improve readability+
−
+
−
p11. Theorem 2(2) : Stressing the uniqueness is strange, given that it follows+
−
trivially from the fact that "lexer" is a function. Maybe state the existence of+
−
a unique POSIX value as corollary.+
−
+
−
*)+
−
+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
+
−
text {*+
−
+
−
Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em+
−
derivative} @{term "der c r"} of a regular expression @{text r} w.r.t.\ a+
−
character~@{text c}, and showed that it gave a simple solution to the+
−
problem of matching a string @{term s} with a regular expression @{term r}:+
−
if the derivative of @{term r} w.r.t.\ (in succession) all the characters of+
−
the string matches the empty string, then @{term r} matches @{term s} (and+
−
{\em vice versa}). The derivative has the property (which may almost be+
−
regarded as its specification) that, for every string @{term s} and regular+
−
expression @{term r} and character @{term c}, one has @{term "cs \<in> L(r)"} if+
−
and only if \mbox{@{term "s \<in> L(der c r)"}}. The beauty of Brzozowski's+
−
derivatives is that they are neatly expressible in any functional language,+
−
and easily definable and reasoned about in theorem provers---the definitions+
−
just consist of inductive datatypes and simple recursive functions. A+
−
completely formalised correctness proof of this matcher in for example HOL4+
−
has been mentioned by Owens and Slind~\cite{Owens2008}. Another one in Isabelle/HOL is part+
−
of the work by Krauss and Nipkow \cite{Krauss2011}. And another one in Coq is given+
−
by Coquand and Siles \cite{Coquand2012}.+
−
+
−
If a regular expression matches a string, then in general there is more than+
−
one way of how the string is matched. There are two commonly used+
−
disambiguation strategies to generate a unique answer: one is called GREEDY+
−
matching \cite{Frisch2004} and the other is POSIX+
−
matching~\cite{Kuklewicz,Sulzmann2014,Vansummeren2006}. For example consider+
−
the string @{term xy} and the regular expression \mbox{@{term "STAR (ALT+
−
(ALT x y) xy)"}}. Either the string can be matched in two `iterations' by+
−
the single letter-regular expressions @{term x} and @{term y}, or directly+
−
in one iteration by @{term xy}. The first case corresponds to GREEDY+
−
matching, which first matches with the left-most symbol and only matches the+
−
next symbol in case of a mismatch (this is greedy in the sense of preferring+
−
instant gratification to delayed repletion). The second case is POSIX+
−
matching, which prefers the longest match.+
−
+
−
In the context of lexing, where an input string needs to be split up into a+
−
sequence of tokens, POSIX is the more natural disambiguation strategy for+
−
what programmers consider basic syntactic building blocks in their programs.+
−
These building blocks are often specified by some regular expressions, say+
−
@{text "r\<^bsub>key\<^esub>"} and @{text "r\<^bsub>id\<^esub>"} for recognising keywords and+
−
identifiers, respectively. There are two underlying (informal) rules behind+
−
tokenising a string in a POSIX fashion according to a collection of regular+
−
expressions:+
−
+
−
\begin{itemize} +
−
\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``maximal munch rule''}):+
−
The longest initial substring matched by any regular expression is taken as+
−
next token.\smallskip+
−
+
−
\item[$\bullet$] \emph{Priority Rule:}+
−
For a particular longest initial substring, the first regular expression+
−
that can match determines the token.+
−
\end{itemize}+
−
+
−
\noindent Consider for example @{text "r\<^bsub>key\<^esub>"} recognising keywords+
−
such as @{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"}+
−
recognising identifiers (say, a single character followed by+
−
characters or numbers).  Then we can form the regular expression+
−
@{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and use POSIX matching to tokenise strings,+
−
say @{text "iffoo"} and @{text "if"}.  For @{text "iffoo"} we obtain+
−
by the Longest Match Rule a single identifier token, not a keyword+
−
followed by an identifier. For @{text "if"} we obtain by the Priority+
−
Rule a keyword token, not an identifier token---even if @{text "r\<^bsub>id\<^esub>"}+
−
matches also.+
−
+
−
One limitation of Brzozowski's matcher is that it only generates a+
−
YES/NO answer for whether a string is being matched by a regular+
−
expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this matcher+
−
to allow generation not just of a YES/NO answer but of an actual+
−
matching, called a [lexical] {\em value}. They give a simple algorithm+
−
to calculate a value that appears to be the value associated with+
−
POSIX matching.  The challenge then is to specify that value, in an+
−
algorithm-independent fashion, and to show that Sulzmann and Lu's+
−
derivative-based algorithm does indeed calculate a value that is+
−
correct according to the specification.+
−
+
−
The answer given by Sulzmann and Lu \cite{Sulzmann2014} is to define a+
−
relation (called an ``order relation'') on the set of values of @{term+
−
r}, and to show that (once a string to be matched is chosen) there is+
−
a maximum element and that it is computed by their derivative-based+
−
algorithm. This proof idea is inspired by work of Frisch and Cardelli+
−
\cite{Frisch2004} on a GREEDY regular expression matching+
−
algorithm. However, we were not able to establish transitivity and+
−
totality for the ``order relation'' by Sulzmann and Lu. In Section+
−
\ref{argu} we identify some inherent problems with their approach (of+
−
which some of the proofs are not published in \cite{Sulzmann2014});+
−
perhaps more importantly, we give a simple inductive (and+
−
algorithm-independent) definition of what we call being a {\em POSIX+
−
value} for a regular expression @{term r} and a string @{term s}; we+
−
show that the algorithm computes such a value and that such a value is+
−
unique. Our proofs are both done by hand and checked in Isabelle/HOL.  The+
−
experience of doing our proofs has been that this mechanical checking+
−
was absolutely essential: this subject area has hidden snares. This+
−
was also noted by Kuklewicz \cite{Kuklewicz} who found that nearly all+
−
POSIX matching implementations are ``buggy'' \cite[Page+
−
203]{Sulzmann2014} and by Grathwohl et al \cite[Page 36]{CrashCourse2014}+
−
who wrote:+
−
+
−
\begin{quote}+
−
\it{}``The POSIX strategy is more complicated than the greedy because of +
−
the dependence on information about the length of matched strings in the +
−
various subexpressions.''+
−
\end{quote}+
−
+
−
%\footnote{The relation @{text "\<ge>\<^bsub>r\<^esub>"} defined by Sulzmann and Lu \cite{Sulzmann2014} +
−
%is a relation on the+
−
%values for the regular expression @{term r}; but it only holds between+
−
%@{term "v\<^sub>1"} and @{term "v\<^sub>2"} in cases where @{term "v\<^sub>1"} and @{term "v\<^sub>2"} have+
−
%the same flattening (underlying string). So a counterexample to totality is+
−
%given by taking two values @{term "v\<^sub>1"} and @{term "v\<^sub>2"} for @{term r} that+
−
%have different flattenings (see Section~\ref{posixsec}). A different+
−
%relation @{text "\<ge>\<^bsub>r,s\<^esub>"} on the set of values for @{term r}+
−
%with flattening @{term s} is definable by the same approach, and is indeed+
−
%total; but that is not what Proposition 1 of \cite{Sulzmann2014} does.}+
−
+
−
+
−
\noindent {\bf Contributions:} We have implemented in Isabelle/HOL the+
−
derivative-based regular expression matching algorithm of+
−
Sulzmann and Lu \cite{Sulzmann2014}. We have proved the correctness of this+
−
algorithm according to our specification of what a POSIX value is (inspired+
−
by work of Vansummeren \cite{Vansummeren2006}). Sulzmann+
−
and Lu sketch in \cite{Sulzmann2014} an informal correctness proof: but to+
−
us it contains unfillable gaps.\footnote{An extended version of+
−
\cite{Sulzmann2014} is available at the website of its first author; this+
−
extended version already includes remarks in the appendix that their+
−
informal proof contains gaps, and possible fixes are not fully worked out.}+
−
Our specification of a POSIX value consists of a simple inductive definition+
−
that given a string and a regular expression uniquely determines this value.+
−
Derivatives as calculated by Brzozowski's method are usually more complex+
−
regular expressions than the initial one; various optimisations are+
−
possible. We prove the correctness when simplifications of @{term "ALT ZERO+
−
r"}, @{term "ALT r ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to+
−
@{term r} are applied.+
−
+
−
*}+
−
+
−
section {* Preliminaries *}+
−
+
−
text {* \noindent Strings in Isabelle/HOL are lists of characters with the+
−
empty string being represented by the empty list, written @{term "[]"}, and+
−
list-cons being written as @{term "DUMMY # DUMMY"}. Often we use the usual+
−
bracket notation for lists also for strings; for example a string consisting+
−
of just a single character @{term c} is written @{term "[c]"}. By using the+
−
type @{type char} for characters we have a supply of finitely many+
−
characters roughly corresponding to the ASCII character set. Regular+
−
expressions are defined as usual as the elements of the following inductive+
−
datatype:+
−
+
−
  \begin{center}+
−
  @{text "r :="}+
−
  @{const "ZERO"} $\mid$+
−
  @{const "ONE"} $\mid$+
−
  @{term "CHAR c"} $\mid$+
−
  @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$+
−
  @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$+
−
  @{term "STAR r"} +
−
  \end{center}+
−
+
−
  \noindent where @{const ZERO} stands for the regular expression that does+
−
  not match any string, @{const ONE} for the regular expression that matches+
−
  only the empty string and @{term c} for matching a character literal. The+
−
  language of a regular expression is also defined as usual by the+
−
  recursive function @{term L} with the six clauses:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l@ {\hspace{3mm}}rcl}+
−
  (1) & @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\+
−
  (2) & @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\+
−
  (3) & @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\+
−
  \end{tabular}+
−
  \hspace{14mm}+
−
  \begin{tabular}{l@ {\hspace{3mm}}rcl}+
−
  (4) & @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  (5) & @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  (6) & @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
  +
−
  \noindent In clause (4) we use the operation @{term "DUMMY ;;+
−
  DUMMY"} for the concatenation of two languages (it is also list-append for+
−
  strings). We use the star-notation for regular expressions and for+
−
  languages (in the last clause above). The star for languages is defined+
−
  inductively by two clauses: @{text "(i)"} the empty string being in+
−
  the star of a language and @{text "(ii)"} if @{term "s\<^sub>1"} is in a+
−
  language and @{term "s\<^sub>2"} in the star of this language, then also @{term+
−
  "s\<^sub>1 @ s\<^sub>2"} is in the star of this language. It will also be convenient+
−
  to use the following notion of a \emph{semantic derivative} (or \emph{left+
−
  quotient}) of a language defined as+
−
  @{thm (lhs) Der_def} $\dn$ @{thm (rhs) Der_def}.+
−
  For semantic derivatives we have the following equations (for example+
−
  mechanically proved in \cite{Krauss2011}):+
−
+
−
  \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}+
−
+
−
+
−
  \noindent \emph{\Brz's derivatives} of regular expressions+
−
  \cite{Brzozowski1964} can be easily defined by two recursive functions:+
−
  the first is from regular expressions to booleans (implementing a test+
−
  when a regular expression can match the empty string), and the second+
−
  takes a regular expression and a character to a (derivative) regular+
−
  expression:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\+
−
  @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\+
−
  @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\+
−
  @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\medskip\\+
−
  +
−
  %\end{tabular}+
−
  %\end{center}+
−
+
−
  %\begin{center}+
−
  %\begin{tabular}{lcl}+
−
  +
−
  @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\+
−
  @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\+
−
  @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\+
−
  @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}+
−
  \end{tabular}+
−
  \end{center}+
−
 +
−
  \noindent+
−
  We may extend this definition to give derivatives w.r.t.~strings:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\+
−
  \end{tabular}+
−
  \hspace{20mm}+
−
  \begin{tabular}{lcl}+
−
  @{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}\label{derprop}\mbox{}\\ +
−
  \begin{tabular}{ll}+
−
  @{text "(1)"} & @{thm (lhs) nullable_correctness} if and only if+
−
  @{thm (rhs) nullable_correctness}, and \\ +
−
  @{text "(2)"} & @{thm[mode=IfThen] der_correctness}.+
−
  \end{tabular}+
−
  \end{proposition}+
−
+
−
  \noindent With this in place it is also very routine to prove that the+
−
  regular expression matcher defined as+
−
  %+
−
  \begin{center}+
−
  @{thm match_def}+
−
  \end{center}+
−
+
−
  \noindent gives a positive answer if and only if @{term "s \<in> L r"}.+
−
  Consequently, this regular expression matching algorithm satisfies the+
−
  usual specification for regular expression matching. While the matcher+
−
  above calculates a provably correct YES/NO answer for whether a regular+
−
  expression matches a string or not, the novel idea of Sulzmann and Lu+
−
  \cite{Sulzmann2014} is to append another phase to this algorithm in order+
−
  to calculate a [lexical] value. We will explain the details next.+
−
+
−
*}+
−
+
−
section {* POSIX Regular Expression Matching\label{posixsec} *}+
−
+
−
text {* +
−
+
−
  The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to define+
−
  values for encoding \emph{how} a regular expression matches a string+
−
  and then define a function on values that mirrors (but inverts) the+
−
  construction of the derivative on regular expressions. \emph{Values}+
−
  are defined as the inductive datatype+
−
+
−
  \begin{center}+
−
  @{text "v :="}+
−
  @{const "Void"} $\mid$+
−
  @{term "val.Char c"} $\mid$+
−
  @{term "Left v"} $\mid$+
−
  @{term "Right v"} $\mid$+
−
  @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ +
−
  @{term "Stars vs"} +
−
  \end{center}  +
−
+
−
  \noindent where we use @{term vs} to stand for a list of+
−
  values. (This is similar to the approach taken by Frisch and+
−
  Cardelli for GREEDY matching \cite{Frisch2004}, and Sulzmann and Lu+
−
  for POSIX matching \cite{Sulzmann2014}). The string underlying a+
−
  value can be calculated by the @{const flat} function, written+
−
  @{term "flat DUMMY"} and defined as:+
−
+
−
  \begin{center}+
−
  \begin{tabular}[t]{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)}+
−
  \end{tabular}\hspace{14mm}+
−
  \begin{tabular}[t]{lcl}+
−
  @{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}+
−
  \\[-8mm]+
−
  @{thm[mode=Axiom] Prf.intros(4)} \qquad+
−
  @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[3mm]+
−
  @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad +
−
  @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[3mm]+
−
  @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[3mm]+
−
  @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad  +
−
  @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}+
−
  \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 @{text+
−
  "Void"}. It is routine to establish how values ``inhabiting'' a regular+
−
  expression correspond to the language of a regular expression, namely+
−
+
−
  \begin{proposition}+
−
  @{thm L_flat_Prf}+
−
  \end{proposition}+
−
+
−
  In general there is more than one value associated with a regular+
−
  expression. In case of POSIX matching the problem is to calculate the+
−
  unique value that satisfies the (informal) POSIX rules from the+
−
  Introduction. Graphically the POSIX value calculation algorithm by+
−
  Sulzmann and Lu can be illustrated by the picture in Figure~\ref{Sulz}+
−
  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. This picture shows the steps required when a+
−
  regular expression, say @{text "r\<^sub>1"}, matches the string @{term+
−
  "[a,b,c]"}. We first build the three derivatives (according to @{term a},+
−
  @{term b} and @{term c}). We then use @{const nullable} to find out+
−
  whether the resulting derivative regular expression @{term "r\<^sub>4"}+
−
  can match the empty string. If yes, we call the function @{const mkeps}+
−
  that produces a value @{term "v\<^sub>4"} for how @{term "r\<^sub>4"} can+
−
  match the empty string (taking into account the POSIX constraints in case+
−
  there are several ways). This function is defined by the clauses:+
−
+
−
\begin{figure}[t]+
−
\begin{center}+
−
\begin{tikzpicture}[scale=2,node distance=1.3cm,+
−
                    every node/.style={minimum size=6mm}]+
−
\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] {@{text "inj r\<^sub>3 c"}};+
−
\node (v2) [left=of v3]{@{term "v\<^sub>2"}};+
−
\draw[->,line width=1mm](v3)--(v2) node[below,midway] {@{text "inj r\<^sub>2 b"}};+
−
\node (v1) [left=of v2] {@{term "v\<^sub>1"}};+
−
\draw[->,line width=1mm](v2)--(v1) node[below,midway] {@{text "inj r\<^sub>1 a"}};+
−
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}};+
−
\end{tikzpicture}+
−
\end{center}+
−
\mbox{}\\[-13mm]+
−
+
−
\caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014},+
−
matching the string @{term "[a,b,c]"}. The first phase (the arrows from +
−
left to right) is \Brz's matcher building successive derivatives. If the +
−
last regular expression is @{term nullable}, then the functions of the +
−
second phase are called (the top-down and right-to-left arrows): 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.+
−
\label{Sulz}}+
−
\end{figure} +
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\+
−
  @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\+
−
  @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent Note that this function needs only to be partially defined,+
−
  namely only for regular expressions that are nullable. In case @{const+
−
  nullable} fails, the string @{term "[a,b,c]"} cannot be matched by @{term+
−
  "r\<^sub>1"} and the null value @{term "None"} is returned. Note also how this function+
−
  makes some subtle choices leading to a POSIX value: for example if an+
−
  alternative regular expression, say @{term "ALT r\<^sub>1 r\<^sub>2"}, can+
−
  match the empty string and furthermore @{term "r\<^sub>1"} can match the+
−
  empty string, then we return a @{text Left}-value. The @{text+
−
  Right}-value will only be returned if @{term "r\<^sub>1"} cannot match the empty+
−
  string.+
−
+
−
  The most interesting idea from Sulzmann and Lu \cite{Sulzmann2014} is+
−
  the construction of a value for how @{term "r\<^sub>1"} can match the+
−
  string @{term "[a,b,c]"} from the value how the last derivative, @{term+
−
  "r\<^sub>4"} in Fig~\ref{Sulz}, can match the empty string. Sulzmann and+
−
  Lu achieve this by stepwise ``injecting back'' the characters into the+
−
  values thus inverting the operation of building derivatives, but on the level+
−
  of values. The corresponding function, called @{term inj}, takes three+
−
  arguments, a regular expression, a character and a value. For example in+
−
  the first (or right-most) @{term inj}-step in Fig~\ref{Sulz} the regular+
−
  expression @{term "r\<^sub>3"}, the character @{term c} from the last+
−
  derivative step and @{term "v\<^sub>4"}, which is the value corresponding+
−
  to the derivative regular expression @{term "r\<^sub>4"}. The result is+
−
  the new value @{term "v\<^sub>3"}. The final result of the algorithm is+
−
  the value @{term "v\<^sub>1"}. The @{term inj} function is defined by recursion on regular+
−
  expressions and by analysing the shape of values (corresponding to +
−
  the derivative regular expressions).+
−
  %+
−
  \begin{center}+
−
  \begin{tabular}{l@ {\hspace{5mm}}lcl}+
−
  (1) & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\+
−
  (2) & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & +
−
      @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\+
−
  (3) & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & +
−
      @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\+
−
  (4) & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ +
−
      & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\+
−
  (5) & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ +
−
      & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\+
−
  (6) & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ +
−
      & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\+
−
  (7) & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ +
−
      & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent To better understand what is going on in this definition it+
−
  might be instructive to look first at the three sequence cases (clauses+
−
  (4)--(6)). In each case we need to construct an ``injected value'' for+
−
  @{term "SEQ r\<^sub>1 r\<^sub>2"}. This must be a value of the form @{term+
−
  "Seq DUMMY DUMMY"}. Recall the clause of the @{text derivative}-function+
−
  for sequence regular expressions:+
−
+
−
  \begin{center}+
−
  @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} $\dn$ @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}+
−
  \end{center}+
−
+
−
  \noindent Consider first the @{text "else"}-branch where the derivative is @{term+
−
  "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore+
−
  be of the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the left-hand+
−
  side in clause~(4) of @{term inj}. In the @{text "if"}-branch the derivative is an+
−
  alternative, namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c+
−
  r\<^sub>2)"}. This means we either have to consider a @{text Left}- or+
−
  @{text Right}-value. In case of the @{text Left}-value we know further it+
−
  must be a value for a sequence regular expression. Therefore the pattern+
−
  we match in the clause (5) is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"},+
−
  while in (6) it is just @{term "Right v\<^sub>2"}. One more interesting+
−
  point is in the right-hand side of clause (6): since in this case the+
−
  regular expression @{text "r\<^sub>1"} does not ``contribute'' to+
−
  matching the string, that means it only matches the empty string, we need to+
−
  call @{const mkeps} in order to construct a value for how @{term "r\<^sub>1"}+
−
  can match this empty string. A similar argument applies for why we can+
−
  expect in the left-hand side of clause (7) that the value is of the form+
−
  @{term "Seq v (Stars vs)"}---the derivative of a star is @{term "SEQ (der c r)+
−
  (STAR r)"}. Finally, the reason for why we can ignore the second argument+
−
  in clause (1) of @{term inj} is that it will only ever be called in cases+
−
  where @{term "c=d"}, but the usual linearity restrictions in patterns do+
−
  not allow us to build this constraint explicitly into our function+
−
  definition.\footnote{Sulzmann and Lu state this clause as @{thm (lhs)+
−
  injval.simps(1)[of "c" "c"]} $\dn$ @{thm (rhs) injval.simps(1)[of "c"]},+
−
  but our deviation is harmless.}+
−
+
−
  The idea of the @{term inj}-function to ``inject'' a character, say+
−
  @{term c}, into a value can be made precise by the first part of the+
−
  following lemma, which shows that the underlying string of an injected+
−
  value has a prepended character @{term c}; the second part shows that the+
−
  underlying string of an @{const mkeps}-value is always the empty string+
−
  (given the regular expression is nullable since otherwise @{text mkeps}+
−
  might not be defined).+
−
+
−
  \begin{lemma}\mbox{}\smallskip\\\label{Prf_injval_flat}+
−
  \begin{tabular}{ll}+
−
  (1) & @{thm[mode=IfThen] Prf_injval_flat}\\+
−
  (2) & @{thm[mode=IfThen] mkeps_flat}+
−
  \end{tabular}+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  Both properties are by routine inductions: the first one can, for example,+
−
  be proved by induction over the definition of @{term derivatives}; the second by+
−
  an induction on @{term r}. There are no interesting cases.\qed+
−
  \end{proof}+
−
+
−
  Having defined the @{const mkeps} and @{text inj} function we can extend+
−
  \Brz's matcher so that a [lexical] value is constructed (assuming the+
−
  regular expression matches the string). The clauses of the Sulzmann and Lu lexer are+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) lexer.simps(1)} & $\dn$ & @{thm (rhs) lexer.simps(1)}\\+
−
  @{thm (lhs) lexer.simps(2)} & $\dn$ & @{text "case"} @{term "lexer (der c r) s"} @{text of}\\+
−
                     & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\+
−
                     & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{term "Some (injval r c v)"}                          +
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent If the regular expression does not match the string, @{const None} is+
−
  returned. If the regular expression \emph{does}+
−
  match the string, then @{const Some} value is returned. One important+
−
  virtue of this algorithm is that it can be implemented with ease in any+
−
  functional programming language and also in Isabelle/HOL. In the remaining+
−
  part of this section we prove that this algorithm is correct.+
−
+
−
  The well-known idea of POSIX matching is informally defined by the longest+
−
  match and priority rule (see Introduction); as correctly argued in \cite{Sulzmann2014}, this+
−
  needs formal specification. Sulzmann and Lu define an ``ordering+
−
  relation'' between values and argue+
−
  that there is a maximum value, as given by the derivative-based algorithm.+
−
  In contrast, we shall introduce a simple inductive definition that+
−
  specifies directly what a \emph{POSIX value} is, incorporating the+
−
  POSIX-specific choices into the side-conditions of our rules. Our+
−
  definition is inspired by the matching relation given by Vansummeren+
−
  \cite{Vansummeren2006}. The relation we define is ternary and written as+
−
  \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating strings, regular expressions and+
−
  values.+
−
  %+
−
  \begin{center}+
−
  \begin{tabular}{c}+
−
  @{thm[mode=Axiom] Posix.intros(1)}@{text "P"}@{term "ONE"} \qquad+
−
  @{thm[mode=Axiom] Posix.intros(2)}@{text "P"}@{term "c"}\medskip\\+
−
  @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}@{text "P+L"}\qquad+
−
  @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}@{text "P+R"}\medskip\\+
−
  $\mprset{flushleft}+
−
   \inferrule+
−
   {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad+
−
    @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\+
−
    @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}+
−
   {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$@{text "PS"}\\+
−
  @{thm[mode=Axiom] Posix.intros(7)}@{text "P[]"}\medskip\\+
−
  $\mprset{flushleft}+
−
   \inferrule+
−
   {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad+
−
    @{thm (prem 2) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad+
−
    @{thm (prem 3) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\+
−
    @{thm (prem 4) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}+
−
   {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$@{text "P\<star>"}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
   \noindent+
−
   We can prove that given a string @{term s} and regular expression @{term+
−
   r}, the POSIX value @{term v} is uniquely determined by @{term "s \<in> r \<rightarrow> v"}.+
−
+
−
  \begin{theorem}\label{posixdeterm}+
−
  @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}+
−
  \end{theorem}+
−
+
−
  \begin{proof} By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and+
−
  a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the+
−
  auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl)+
−
  Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily+
−
  established by inductions.\qed +
−
  \end{proof}+
−
+
−
  \noindent+
−
  We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two+
−
  informal POSIX rules shown in the Introduction: Consider for example the+
−
  rules @{text "P+L"} and @{text "P+R"} where the POSIX value for a string+
−
  and an alternative regular expression, that is @{term "(s, ALT r\<^sub>1 r\<^sub>2)"},+
−
  is specified---it is always a @{text "Left"}-value, \emph{except} when the+
−
  string to be matched is not in the language of @{term "r\<^sub>1"}; only then it+
−
  is a @{text Right}-value (see the side-condition in @{text "P+R"}).+
−
  Interesting is also the rule for sequence regular expressions (@{text+
−
  "PS"}). The first two premises state that @{term "v\<^sub>1"} and @{term "v\<^sub>2"}+
−
  are the POSIX values for @{term "(s\<^sub>1, r\<^sub>1)"} and @{term "(s\<^sub>2, r\<^sub>2)"}+
−
  respectively. Consider now the third premise and note that the POSIX value+
−
  of this rule should match the string @{term "s\<^sub>1 @ s\<^sub>2"}. According to the+
−
  longest match rule, we want that the @{term "s\<^sub>1"} is the longest initial+
−
  split of \mbox{@{term "s\<^sub>1 @ s\<^sub>2"}} such that @{term "s\<^sub>2"} is still recognised+
−
  by @{term "r\<^sub>2"}. Let us assume, contrary to the third premise, that there+
−
  \emph{exist} an @{term "s\<^sub>3"} and @{term "s\<^sub>4"} such that @{term "s\<^sub>2"}+
−
  can be split up into a non-empty string @{term "s\<^sub>3"} and a possibly empty+
−
  string @{term "s\<^sub>4"}. Moreover the longer string @{term "s\<^sub>1 @ s\<^sub>3"} can be+
−
  matched by @{text "r\<^sub>1"} and the shorter @{term "s\<^sub>4"} can still be+
−
  matched by @{term "r\<^sub>2"}. In this case @{term "s\<^sub>1"} would \emph{not} be the+
−
  longest initial split of \mbox{@{term "s\<^sub>1 @ s\<^sub>2"}} and therefore @{term "Seq v\<^sub>1+
−
  v\<^sub>2"} cannot be a POSIX value for @{term "(s\<^sub>1 @ s\<^sub>2, SEQ r\<^sub>1 r\<^sub>2)"}. +
−
  The main point is that this side-condition ensures the longest +
−
  match rule is satisfied.+
−
+
−
  A similar condition is imposed on the POSIX value in the @{text+
−
  "P\<star>"}-rule. Also there we want that @{term "s\<^sub>1"} is the longest initial+
−
  split of @{term "s\<^sub>1 @ s\<^sub>2"} and furthermore the corresponding value+
−
  @{term v} cannot be flattened to the empty string. In effect, we require+
−
  that in each ``iteration'' of the star, some non-empty substring needs to+
−
  be ``chipped'' away; only in case of the empty string we accept @{term+
−
  "Stars []"} as the POSIX value.+
−
+
−
  Next is the lemma that shows the function @{term "mkeps"} calculates+
−
  the POSIX value for the empty string and a nullable regular expression.+
−
+
−
  \begin{lemma}\label{lemmkeps}+
−
  @{thm[mode=IfThen] Posix_mkeps}+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
  By routine induction on @{term r}.\qed +
−
  \end{proof}+
−
+
−
  \noindent+
−
  The central lemma for our POSIX relation is that the @{text inj}-function+
−
  preserves POSIX values.+
−
+
−
  \begin{lemma}\label{Posix2}+
−
  @{thm[mode=IfThen] Posix_injval}+
−
  \end{lemma}+
−
+
−
  \begin{proof}+
−
+
−
  By induction on @{text r}. Suppose @{term "r = ALT r\<^sub>1 r\<^sub>2"}. There are+
−
  two subcases, namely @{text "(a)"} \mbox{@{term "v = Left v'"}} and @{term+
−
  "s \<in> der c r\<^sub>1 \<rightarrow> v'"}; and @{text "(b)"} @{term "v = Right v'"}, @{term+
−
  "s \<notin> L (der c r\<^sub>1)"} and @{term "s \<in> der c r\<^sub>2 \<rightarrow> v'"}. In @{text "(a)"} we+
−
  know @{term "s \<in> der c r\<^sub>1 \<rightarrow> v'"}, from which we can infer @{term "(c # s)+
−
  \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v'"} by induction hypothesis and hence @{term "(c #+
−
  s) \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> injval (ALT r\<^sub>1 r\<^sub>2) c (Left v')"} as needed. Similarly+
−
  in subcase @{text "(b)"} where, however, in addition we have to use+
−
  Prop.~\ref{derprop}(2) in order to infer @{term "c # s \<notin> L r\<^sub>1"} from @{term+
−
  "s \<notin> L (der c r\<^sub>1)"}.+
−
+
−
  Suppose @{term "r = SEQ r\<^sub>1 r\<^sub>2"}. There are three subcases:+
−
  +
−
  \begin{quote}+
−
  \begin{description}+
−
  \item[@{text "(a)"}] @{term "v = Left (Seq v\<^sub>1 v\<^sub>2)"} and @{term "nullable r\<^sub>1"} +
−
  \item[@{text "(b)"}] @{term "v = Right v\<^sub>1"} and @{term "nullable r\<^sub>1"} +
−
  \item[@{text "(c)"}] @{term "v = Seq v\<^sub>1 v\<^sub>2"} and @{term "\<not> nullable r\<^sub>1"} +
−
  \end{description}+
−
  \end{quote}+
−
+
−
  \noindent For @{text "(a)"} we know @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} and+
−
  @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} as well as+
−
  %+
−
  \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\]+
−
+
−
  \noindent From the latter we can infer by Prop.~\ref{derprop}(2):+
−
  %+
−
  \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\]+
−
+
−
  \noindent We can use the induction hypothesis for @{text "r\<^sub>1"} to obtain+
−
  @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}. Putting this all together allows us to infer+
−
  @{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}. The case @{text "(c)"}+
−
  is similar.+
−
+
−
  For @{text "(b)"} we know @{term "s \<in> der c r\<^sub>2 \<rightarrow> v\<^sub>1"} and +
−
  @{term "s\<^sub>1 @ s\<^sub>2 \<notin> L (SEQ (der c r\<^sub>1) r\<^sub>2)"}. From the former+
−
  we have @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> (injval r\<^sub>2 c v\<^sub>1)"} by induction hypothesis+
−
  for @{term "r\<^sub>2"}. From the latter we can infer+
−
  %+
−
  \[@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}\]+
−
+
−
  \noindent By Lem.~\ref{lemmkeps} we know @{term "[] \<in> r\<^sub>1 \<rightarrow> (mkeps r\<^sub>1)"}+
−
  holds. Putting this all together, we can conclude with @{term "(c #+
−
  s) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (mkeps r\<^sub>1) (injval r\<^sub>2 c v\<^sub>1)"}, as required.+
−
+
−
  Finally suppose @{term "r = STAR r\<^sub>1"}. This case is very similar to the+
−
  sequence case, except that we need to also ensure that @{term "flat (injval r\<^sub>1+
−
  c v\<^sub>1) \<noteq> []"}. This follows from @{term "(c # s\<^sub>1)+
−
  \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"}  (which in turn follows from @{term "s\<^sub>1 \<in> der c+
−
  r\<^sub>1 \<rightarrow> v\<^sub>1"} and the induction hypothesis).\qed+
−
  \end{proof}+
−
+
−
  \noindent+
−
  With Lem.~\ref{Posix2} in place, it is completely routine to establish+
−
  that the Sulzmann and Lu lexer satisfies our specification (returning+
−
  the null value @{term "None"} iff the string is not in the language of the regular expression,+
−
  and returning a unique POSIX value iff the string \emph{is} in the language):+
−
+
−
  \begin{theorem}\mbox{}\smallskip\\\label{lexercorrect}+
−
  \begin{tabular}{ll}+
−
  (1) & @{thm (lhs) lexer_correct_None} if and only if @{thm (rhs) lexer_correct_None}\\+
−
  (2) & @{thm (lhs) lexer_correct_Some} if and only if @{thm (rhs) lexer_correct_Some}\\+
−
  \end{tabular}+
−
  \end{theorem}+
−
+
−
  \begin{proof}+
−
  By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed  +
−
  \end{proof}+
−
+
−
  \noindent This concludes our correctness proof. Note that we have not+
−
  changed the algorithm of Sulzmann and Lu,\footnote{All deviations we+
−
  introduced are harmless.} but introduced our own specification for what a+
−
  correct result---a POSIX value---should be. A strong point in favour of+
−
  Sulzmann and Lu's algorithm is that it can be extended in various ways.+
−
+
−
*}+
−
+
−
section {* Extensions and Optimisations*}+
−
+
−
text {*+
−
+
−
  If we are interested in tokenising a string, then we need to not just+
−
  split up the string into tokens, but also ``classify'' the tokens (for+
−
  example whether it is a keyword or an identifier). This can be done with+
−
  only minor modifications to the algorithm by introducing \emph{record+
−
  regular expressions} and \emph{record values} (for example+
−
  \cite{Sulzmann2014b}):+
−
+
−
  \begin{center}  +
−
  @{text "r :="}+
−
  @{text "..."} $\mid$+
−
  @{text "(l : r)"} \qquad\qquad+
−
  @{text "v :="}+
−
  @{text "..."} $\mid$+
−
  @{text "(l : v)"}+
−
  \end{center}+
−
  +
−
  \noindent where @{text l} is a label, say a string, @{text r} a regular+
−
  expression and @{text v} a value. All functions can be smoothly extended+
−
  to these regular expressions and values. For example \mbox{@{text "(l :+
−
  r)"}} is nullable iff @{term r} is, and so on. The purpose of the record+
−
  regular expression is to mark certain parts of a regular expression and+
−
  then record in the calculated value which parts of the string were matched+
−
  by this part. The label can then serve as classification for the tokens.+
−
  For this recall the regular expression @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} for+
−
  keywords and identifiers from the Introduction. With the record regular+
−
  expression we can form \mbox{@{text "((key : r\<^bsub>key\<^esub>) + (id : r\<^bsub>id\<^esub>))\<^sup>\<star>"}}+
−
  and then traverse the calculated value and only collect the underlying+
−
  strings in record values. With this we obtain finite sequences of pairs of+
−
  labels and strings, for example+
−
+
−
  \[@{text "(l\<^sub>1 : s\<^sub>1), ..., (l\<^sub>n : s\<^sub>n)"}\]+
−
  +
−
  \noindent from which tokens with classifications (keyword-token,+
−
  identifier-token and so on) can be extracted.+
−
+
−
  Derivatives as calculated by \Brz's method are usually more complex+
−
  regular expressions than the initial one; the result is that the+
−
  derivative-based matching and lexing algorithms are often abysmally slow.+
−
  However, various optimisations are possible, such as the simplifications+
−
  of @{term "ALT ZERO r"}, @{term "ALT r ZERO"}, @{term "SEQ ONE r"} and+
−
  @{term "SEQ r ONE"} to @{term r}. These simplifications can speed up the+
−
  algorithms considerably, as noted in \cite{Sulzmann2014}. One of the+
−
  advantages of having a simple specification and correctness proof is that+
−
  the latter can be refined to prove the correctness of such simplification+
−
  steps.+
−
+
−
  While the simplification of regular expressions according to +
−
  rules like+
−
+
−
  \begin{equation}\label{Simpl}+
−
  \begin{array}{lcllcllcllcl}+
−
  @{term "ALT ZERO r"} & @{text "\<Rightarrow>"} & @{term r} \hspace{8mm}%\\+
−
  @{term "ALT r ZERO"} & @{text "\<Rightarrow>"} & @{term r} \hspace{8mm}%\\+
−
  @{term "SEQ ONE r"}  & @{text "\<Rightarrow>"} & @{term r} \hspace{8mm}%\\+
−
  @{term "SEQ r ONE"}  & @{text "\<Rightarrow>"} & @{term r}+
−
  \end{array}+
−
  \end{equation}+
−
+
−
  \noindent is well understood, there is an obstacle with the POSIX value+
−
  calculation algorithm by Sulzmann and Lu: if we build a derivative regular+
−
  expression and then simplify it, we will calculate a POSIX value for this+
−
  simplified derivative regular expression, \emph{not} for the original (unsimplified)+
−
  derivative regular expression. Sulzmann and Lu \cite{Sulzmann2014} overcome this obstacle by+
−
  not just calculating a simplified regular expression, but also calculating+
−
  a \emph{rectification function} that ``repairs'' the incorrect value.+
−
  +
−
  The rectification functions can be (slightly clumsily) implemented  in+
−
  Isabelle/HOL as follows using some auxiliary functions:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) F_RIGHT.simps(1)} & $\dn$ & @{text "Right (f v)"}\\+
−
  @{thm (lhs) F_LEFT.simps(1)} & $\dn$ & @{text "Left (f v)"}\\+
−
  +
−
  @{thm (lhs) F_ALT.simps(1)} & $\dn$ & @{text "Right (f\<^sub>2 v)"}\\+
−
  @{thm (lhs) F_ALT.simps(2)} & $\dn$ & @{text "Left (f\<^sub>1 v)"}\\+
−
  +
−
  @{thm (lhs) F_SEQ1.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 ()) (f\<^sub>2 v)"}\\+
−
  @{thm (lhs) F_SEQ2.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v) (f\<^sub>2 ())"}\\+
−
  @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}\medskip\\+
−
  %\end{tabular}+
−
  %+
−
  %\begin{tabular}{lcl}+
−
  @{term "simp_ALT (ZERO, DUMMY) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_RIGHT f\<^sub>2)"}\\+
−
  @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, DUMMY)"} & $\dn$ & @{term "(r\<^sub>1, F_LEFT f\<^sub>1)"}\\+
−
  @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"}\\+
−
  @{term "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"}\\+
−
  @{term "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"}\\+
−
  @{term "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The functions @{text "simp\<^bsub>Alt\<^esub>"} and @{text "simp\<^bsub>Seq\<^esub>"} encode the simplification rules+
−
  in \eqref{Simpl} and compose the rectification functions (simplifications can occur+
−
  deep inside the regular expression). The main simplification function is then +
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{term "simp (ALT r\<^sub>1 r\<^sub>2)"} & $\dn$ & @{term "simp_ALT (simp r\<^sub>1) (simp r\<^sub>2)"}\\+
−
  @{term "simp (SEQ r\<^sub>1 r\<^sub>2)"} & $\dn$ & @{term "simp_SEQ (simp r\<^sub>1) (simp r\<^sub>2)"}\\+
−
  @{term "simp r"} & $\dn$ & @{term "(r, id)"}\\+
−
  \end{tabular}+
−
  \end{center} +
−
+
−
  \noindent where @{term "id"} stands for the identity function. The+
−
  function @{const simp} returns a simplified regular expression and a corresponding+
−
  rectification function. Note that we do not simplify under stars: this+
−
  seems to slow down the algorithm, rather than speed it up. The optimised+
−
  lexer is then given by the clauses:+
−
  +
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{thm (lhs) slexer.simps(1)} & $\dn$ & @{thm (rhs) slexer.simps(1)}\\+
−
  @{thm (lhs) slexer.simps(2)} & $\dn$ & +
−
                         @{text "let (r\<^sub>s, f\<^sub>r) = simp (r "}$\backslash$@{text " c) in"}\\+
−
                     & & @{text "case"} @{term "slexer r\<^sub>s s"} @{text of}\\+
−
                     & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\+
−
                     & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{text "Some (inj r c (f\<^sub>r v))"}                          +
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  In the second clause we first calculate the derivative @{term "der c r"}+
−
  and then simplify the result. This gives us a simplified derivative+
−
  @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The lexer+
−
  is then recursively called with the simplified derivative, but before+
−
  we inject the character @{term c} into the value @{term v}, we need to rectify+
−
  @{term v} (that is construct @{term "f\<^sub>r v"}). Before we can establish the correctness+
−
  of @{term "slexer"}, we need to show that simplification preserves the language+
−
  and simplification preserves our POSIX relation once the value is rectified+
−
  (recall @{const "simp"} generates a regular expression / rectification function pair):+
−
+
−
  \begin{lemma}\mbox{}\smallskip\\\label{slexeraux}+
−
  \begin{tabular}{ll}+
−
  (1) & @{thm L_fst_simp[symmetric]}\\+
−
  (2) & @{thm[mode=IfThen] Posix_simp}+
−
  \end{tabular}+
−
  \end{lemma}+
−
+
−
  \begin{proof} Both are by induction on @{text r}. There is no+
−
  interesting case for the first statement. For the second statement,+
−
  of interest are the @{term "r = ALT r\<^sub>1 r\<^sub>2"} and @{term "r = SEQ r\<^sub>1+
−
  r\<^sub>2"} cases. In each case we have to analyse four subcases whether+
−
  @{term "fst (simp r\<^sub>1)"} and @{term "fst (simp r\<^sub>2)"} equals @{const+
−
  ZERO} (respectively @{const ONE}). For example for @{term "r = ALT+
−
  r\<^sub>1 r\<^sub>2"}, consider the subcase @{term "fst (simp r\<^sub>1) = ZERO"} and+
−
  @{term "fst (simp r\<^sub>2) \<noteq> ZERO"}. By assumption we know @{term "s \<in>+
−
  fst (simp (ALT r\<^sub>1 r\<^sub>2)) \<rightarrow> v"}. From this we can infer @{term "s \<in> fst (simp r\<^sub>2) \<rightarrow> v"}+
−
  and by IH also (*) @{term "s \<in> r\<^sub>2 \<rightarrow> (snd (simp r\<^sub>2) v)"}. Given @{term "fst (simp r\<^sub>1) = ZERO"}+
−
  we know @{term "L (fst (simp r\<^sub>1)) = {}"}. By the first statement+
−
  @{term "L r\<^sub>1"} is the empty set, meaning (**) @{term "s \<notin> L r\<^sub>1"}.+
−
  Taking (*) and (**) together gives by the \mbox{@{text "P+R"}}-rule +
−
  @{term "s \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> Right (snd (simp r\<^sub>2) v)"}. In turn this+
−
  gives @{term "s \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> snd (simp (ALT r\<^sub>1 r\<^sub>2)) v"} as we need to show.+
−
  The other cases are similar.\qed+
−
  \end{proof}+
−
+
−
  \noindent We can now prove relatively straightforwardly that the+
−
  optimised lexer produces the expected result:+
−
+
−
  \begin{theorem}+
−
  @{thm slexer_correctness}+
−
  \end{theorem}+
−
+
−
  \begin{proof} By induction on @{term s} generalising over @{term+
−
  r}. The case @{term "[]"} is trivial. For the cons-case suppose the+
−
  string is of the form @{term "c # s"}. By induction hypothesis we+
−
  know @{term "slexer r s = lexer r s"} holds for all @{term r} (in+
−
  particular for @{term "r"} being the derivative @{term "der c+
−
  r"}). Let @{term "r\<^sub>s"} be the simplified derivative regular expression, that is @{term+
−
  "fst (simp (der c r))"}, and @{term "f\<^sub>r"} be the rectification+
−
  function, that is @{term "snd (simp (der c r))"}.  We distinguish the cases+
−
  whether (*) @{term "s \<in> L (der c r)"} or not. In the first case we+
−
  have by Thm.~\ref{lexercorrect}(2) a value @{term "v"} so that @{term+
−
  "lexer (der c r) s = Some v"} and @{term "s \<in> der c r \<rightarrow> v"} hold.+
−
  By Lem.~\ref{slexeraux}(1) we can also infer from~(*) that @{term "s+
−
  \<in> L r\<^sub>s"} holds.  Hence we know by Thm.~\ref{lexercorrect}(2) that+
−
  there exists a @{term "v'"} with @{term "lexer r\<^sub>s s = Some v'"} and+
−
  @{term "s \<in> r\<^sub>s \<rightarrow> v'"}. From the latter we know by+
−
  Lem.~\ref{slexeraux}(2) that @{term "s \<in> der c r \<rightarrow> (f\<^sub>r v')"} holds.+
−
  By the uniqueness of the POSIX relation (Thm.~\ref{posixdeterm}) we+
−
  can infer that @{term v} is equal to @{term "f\<^sub>r v'"}---that is the +
−
  rectification function applied to @{term "v'"}+
−
  produces the original @{term "v"}.  Now the case follows by the+
−
  definitions of @{const lexer} and @{const slexer}.+
−
+
−
  In the second case where @{term "s \<notin> L (der c r)"} we have that+
−
  @{term "lexer (der c r) s = None"} by Thm.~\ref{lexercorrect}(1).  We+
−
  also know by Lem.~\ref{slexeraux}(1) that @{term "s \<notin> L r\<^sub>s"}. Hence+
−
  @{term "lexer r\<^sub>s s = None"} by Thm.~\ref{lexercorrect}(1) and+
−
  by IH then also @{term "slexer r\<^sub>s s = None"}. With this we can+
−
  conclude in this case too.\qed   +
−
+
−
  \end{proof} +
−
*}+
−
+
−
section {* The Correctness Argument by Sulzmann and Lu\label{argu} *}+
−
+
−
text {*+
−
%  \newcommand{\greedy}{\succcurlyeq_{gr}}+
−
 \newcommand{\posix}{>}+
−
+
−
  An extended version of \cite{Sulzmann2014} is available at the website of+
−
  its first author; this includes some ``proofs'', claimed in+
−
  \cite{Sulzmann2014} to be ``rigorous''. Since these are evidently not in+
−
  final form, we make no comment thereon, preferring to give general reasons+
−
  for our belief that the approach of \cite{Sulzmann2014} is problematic.+
−
  Their central definition is an ``ordering relation'' defined by the+
−
  rules (slightly adapted to fit our notation):+
−
+
−
\begin{center}  +
−
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	+
−
@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &+
−
@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\+
−
+
−
@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) &+
−
@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\+
−
+
−
@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) &+
−
@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\+
−
+
−
@{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) &+
−
@{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\+
−
+
−
@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) &+
−
@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4)+
−
\end{tabular}+
−
\end{center}+
−
+
−
  \noindent The idea behind the rules (A1) and (A2), for example, is that a+
−
  @{text Left}-value is bigger than a @{text Right}-value, if the underlying+
−
  string of the @{text Left}-value is longer or of equal length to the+
−
  underlying string of the @{text Right}-value. The order is reversed,+
−
  however, if the @{text Right}-value can match a longer string than a+
−
  @{text Left}-value. In this way the POSIX value is supposed to be the+
−
  biggest value for a given string and regular expression.+
−
+
−
  Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch+
−
  and Cardelli from where they have taken the idea for their correctness+
−
  proof. Frisch and Cardelli introduced a similar ordering for GREEDY+
−
  matching and they showed that their GREEDY matching algorithm always+
−
  produces a maximal element according to this ordering (from all possible+
−
  solutions). The only difference between their GREEDY ordering and the+
−
  ``ordering'' by Sulzmann and Lu is that GREEDY always prefers a @{text+
−
  Left}-value over a @{text Right}-value, no matter what the underlying+
−
  string is. This seems to be only a very minor difference, but it has+
−
  drastic consequences in terms of what properties both orderings enjoy.+
−
  What is interesting for our purposes is that the properties reflexivity,+
−
  totality and transitivity for this GREEDY ordering can be proved+
−
  relatively easily by induction.+
−
+
−
  These properties of GREEDY, however, do not transfer to the POSIX+
−
  ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. +
−
  To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is+
−
  not defined inductively, but as @{term "v\<^sub>1 = v\<^sub>2"} or @{term "(v\<^sub>1 >r+
−
  v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}. This means that @{term "v\<^sub>1+
−
  >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)+
−
  (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''+
−
  formulation, for example:+
−
+
−
  \begin{falsehood}+
−
  Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.+
−
  If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}+
−
  then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.+
−
  \end{falsehood}+
−
+
−
  \noindent If formulated in this way, then there are various counter+
−
  examples: For example let @{term r} be @{text "a + ((a + a)\<cdot>(a + \<zero>))"}+
−
  then the @{term "v\<^sub>1"}, @{term "v\<^sub>2"} and @{term "v\<^sub>3"} below are values+
−
  of @{term r}:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{lcl}+
−
  @{term "v\<^sub>1"} & $=$ & @{term "Left(Char a)"}\\+
−
  @{term "v\<^sub>2"} & $=$ & @{term "Right(Seq (Left(Char a)) (Right Void))"}\\+
−
  @{term "v\<^sub>3"} & $=$ & @{term "Right(Seq (Right(Char a)) (Left(Char a)))"}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent Moreover @{term "v\<^sub>1 >(r::rexp) v\<^sub>2"} and @{term "v\<^sub>2 >(r::rexp)+
−
  v\<^sub>3"}, but \emph{not} @{term "v\<^sub>1 >(r::rexp) v\<^sub>3"}! The reason is that+
−
  although @{term "v\<^sub>3"} is a @{text "Right"}-value, it can match a longer+
−
  string, namely @{term "flat v\<^sub>3 = [a,a]"}, while @{term "flat v\<^sub>1"} (and+
−
  @{term "flat v\<^sub>2"}) matches only @{term "[a]"}. So transitivity in this+
−
  formulation does not hold---in this example actually @{term "v\<^sub>3+
−
  >(r::rexp) v\<^sub>1"}!+
−
+
−
  Sulzmann and Lu ``fix'' this problem by weakening the transitivity+
−
  property. They require in addition that the underlying strings are of the+
−
  same length. This excludes the counter example above and any+
−
  counter-example we were able to find (by hand and by machine). Thus the+
−
  transitivity lemma should be formulated as:+
−
+
−
  \begin{conject}+
−
  Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"},+
−
  and also @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}.\\+
−
  If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}+
−
  then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}.+
−
  \end{conject}+
−
+
−
  \noindent While we agree with Sulzmann and Lu that this property+
−
  probably(!) holds, proving it seems not so straightforward: although one+
−
  begins with the assumption that the values have the same flattening, this+
−
  cannot be maintained as one descends into the induction. This is a problem+
−
  that occurs in a number of places in the proofs by Sulzmann and Lu.+
−
+
−
  Although they do not give an explicit proof of the transitivity property,+
−
  they give a closely related property about the existence of maximal+
−
  elements. They state that this can be verified by an induction on $r$. We+
−
  disagree with this as we shall show next in case of transitivity. The case+
−
  where the reasoning breaks down is the sequence case, say @{term "SEQ r\<^sub>1 r\<^sub>2"}.+
−
  The induction hypotheses in this case are+
−
+
−
\begin{center}+
−
\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}+
−
\begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}+
−
IH @{term "r\<^sub>1"}:\\+
−
@{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."} \\+
−
  & @{term "\<turnstile> v\<^sub>1 : r\<^sub>1"}\;@{text "\<and>"}+
−
    @{term "\<turnstile> v\<^sub>2 : r\<^sub>1"}\;@{text "\<and>"}+
−
    @{term "\<turnstile> v\<^sub>3 : r\<^sub>1"}\\+
−
  & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\+
−
  & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>1::rexp) v\<^sub>3"}\medskip\\+
−
  & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>1::rexp) v\<^sub>3"}+
−
\end{tabular} &+
−
\begin{tabular}{@ {}l@ {\hspace{-7mm}}l@ {}}+
−
IH @{term "r\<^sub>2"}:\\+
−
@{text "\<forall> v\<^sub>1, v\<^sub>2, v\<^sub>3."}\\ +
−
  & @{term "\<turnstile> v\<^sub>1 : r\<^sub>2"}\;@{text "\<and>"}+
−
    @{term "\<turnstile> v\<^sub>2 : r\<^sub>2"}\;@{text "\<and>"}+
−
    @{term "\<turnstile> v\<^sub>3 : r\<^sub>2"}\\+
−
  & @{text "\<and>"} @{text "|v\<^sub>1| = |v\<^sub>2| = |v\<^sub>3|"}\\+
−
  & @{text "\<and>"} @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>2 \<and> v\<^sub>2 >(r\<^sub>2::rexp) v\<^sub>3"}\medskip\\+
−
  & $\Rightarrow$ @{term "v\<^sub>1 >(r\<^sub>2::rexp) v\<^sub>3"}+
−
\end{tabular}+
−
\end{tabular}+
−
\end{center} +
−
+
−
  \noindent We can assume that+
−
  %+
−
  \begin{equation}+
−
  @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}+
−
  \qquad\textrm{and}\qquad+
−
  @{term "(Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2) (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}+
−
  \label{assms}+
−
  \end{equation}+
−
+
−
  \noindent hold, and furthermore that the values have equal length, namely:+
−
  %+
−
  \begin{equation}+
−
  @{term "flat (Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) = flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r))"}+
−
  \qquad\textrm{and}\qquad+
−
  @{term "flat (Seq (v\<^sub>2\<^sub>l) (v\<^sub>2\<^sub>r)) = flat (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"}+
−
  \label{lens}+
−
  \end{equation} +
−
+
−
  \noindent We need to show that @{term "(Seq (v\<^sub>1\<^sub>l) (v\<^sub>1\<^sub>r)) >(SEQ r\<^sub>1 r\<^sub>2)+
−
  (Seq (v\<^sub>3\<^sub>l) (v\<^sub>3\<^sub>r))"} holds. We can proceed by analysing how the+
−
  assumptions in \eqref{assms} have arisen. There are four cases. Let us+
−
  assume we are in the case where we know+
−
+
−
  \[+
−
  @{term "v\<^sub>1\<^sub>l >(r\<^sub>1::rexp) v\<^sub>2\<^sub>l"}+
−
  \qquad\textrm{and}\qquad+
−
  @{term "v\<^sub>2\<^sub>l >(r\<^sub>1::rexp) v\<^sub>3\<^sub>l"}+
−
  \]+
−
+
−
  \noindent and also know the corresponding inhabitation judgements. This is+
−
  exactly a case where we would like to apply the induction hypothesis+
−
  IH~$r_1$. But we cannot! We still need to show that @{term "flat (v\<^sub>1\<^sub>l) =+
−
  flat(v\<^sub>2\<^sub>l)"} and @{term "flat(v\<^sub>2\<^sub>l) = flat(v\<^sub>3\<^sub>l)"}. We know from+
−
  \eqref{lens} that the lengths of the sequence values are equal, but from+
−
  this we cannot infer anything about the lengths of the component values.+
−
  Indeed in general they will be unequal, that is+
−
+
−
  \[+
−
  @{term "flat(v\<^sub>1\<^sub>l) \<noteq> flat(v\<^sub>2\<^sub>l)"}  +
−
  \qquad\textrm{and}\qquad+
−
  @{term "flat(v\<^sub>1\<^sub>r) \<noteq> flat(v\<^sub>2\<^sub>r)"}+
−
  \]+
−
+
−
  \noindent but still \eqref{lens} will hold. Now we are stuck, since the IH+
−
  does not apply. As said, this problem where the induction hypothesis does+
−
  not apply arises in several places in the proof of Sulzmann and Lu, not+
−
  just for proving transitivity.+
−
+
−
*}+
−
+
−
section {* Conclusion *}+
−
+
−
text {*+
−
+
−
  We have implemented the POSIX value calculation algorithm introduced by+
−
  Sulzmann and Lu+
−
  \cite{Sulzmann2014}. Our implementation is nearly identical to the+
−
  original and all modifications we introduced are harmless (like our char-clause for+
−
  @{text inj}). We have proved this algorithm to be correct, but correct+
−
  according to our own specification of what POSIX values are. Our+
−
  specification (inspired from work by Vansummeren \cite{Vansummeren2006}) appears to be+
−
  much simpler than in \cite{Sulzmann2014} and our proofs are nearly always+
−
  straightforward. We have attempted to formalise the original proof+
−
  by Sulzmann and Lu \cite{Sulzmann2014}, but we believe it contains+
−
  unfillable gaps. In the online version of \cite{Sulzmann2014}, the authors+
−
  already acknowledge some small problems, but our experience suggests+
−
  that there are more serious problems. +
−
  +
−
  Having proved the correctness of the POSIX lexing algorithm in+
−
  \cite{Sulzmann2014}, which lessons have we learned? Well, this is a+
−
  perfect example for the importance of the \emph{right} definitions. We+
−
  have (on and off) explored mechanisations as soon as first versions+
−
  of \cite{Sulzmann2014} appeared, but have made little progress with+
−
  turning the relatively detailed proof sketch in \cite{Sulzmann2014} into a+
−
  formalisable proof. Having seen \cite{Vansummeren2006} and adapted the+
−
  POSIX definition given there for the algorithm by Sulzmann and Lu made all+
−
  the difference: the proofs, as said, are nearly straightforward. The+
−
  question remains whether the original proof idea of \cite{Sulzmann2014},+
−
  potentially using our result as a stepping stone, can be made to work?+
−
  Alas, we really do not know despite considerable effort.+
−
+
−
+
−
  Closely related to our work is an automata-based lexer formalised by+
−
  Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest+
−
  initial substrings, but Nipkow's algorithm is not completely+
−
  computational. The algorithm by Sulzmann and Lu, in contrast, can be+
−
  implemented with ease in any functional language. A bespoke lexer for the+
−
  Imp-language is formalised in Coq as part of the Software Foundations book+
−
  by Pierce et al \cite{Pierce2015}. The disadvantage of such bespoke lexers is that they+
−
  do not generalise easily to more advanced features.+
−
  Our formalisation is available from+
−
  \url{http://www.inf.kcl.ac.uk/staff/urbanc/lex}.\medskip+
−
+
−
  \noindent+
−
  {\bf Acknowledgements:}+
−
  We are very grateful to Martin Sulzmann for his comments on our work and +
−
  moreover patiently explaining to us the details in \cite{Sulzmann2014}. We+
−
  also received very helpful comments from James Cheney and anonymous referees.+
−
  \small+
−
  \bibliographystyle{plain}+
−
  \bibliography{root}+
−
+
−
*}+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−