--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Journal/PaperExt.thy Tue Aug 21 14:14:19 2018 +0100
@@ -0,0 +1,323 @@
+(*<*)
+theory PaperExt
+imports
+ (*"../LexerExt"*)
+ (*"../PositionsExt"*)
+ "~~/src/HOL/Library/LaTeXsugar"
+begin
+(*>*)
+
+(*
+declare [[show_question_marks = false]]
+declare [[eta_contract = false]]
+
+abbreviation
+ "der_syn r c \<equiv> der c r"
+
+abbreviation
+ "ders_syn r s \<equiv> ders s r"
+
+
+notation (latex output)
+ If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and
+ Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and
+
+ ZERO ("\<^bold>0" 81) and
+ ONE ("\<^bold>1" 81) and
+ CHAR ("_" [1000] 80) and
+ ALT ("_ + _" [77,77] 78) and
+ SEQ ("_ \<cdot> _" [77,77] 78) and
+ STAR ("_\<^sup>\<star>" [78] 78) and
+ NTIMES ("_\<^bsup>'{_'}\<^esup>" [78, 50] 80) and
+ FROMNTIMES ("_\<^bsup>'{_..'}\<^esup>" [78, 50] 80) and
+ UPNTIMES ("_\<^bsup>'{.._'}\<^esup>" [78, 50] 80) and
+ NMTIMES ("_\<^bsup>'{_.._'}\<^esup>" [78, 50,50] 80) and
+
+ val.Void ("Empty" 78) 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 _" [1000] 78) and
+
+ L ("L'(_')" [10] 78) and
+ LV ("LV _ _" [80,73] 78) and
+ der_syn ("_\\_" [79, 1000] 76) and
+ ders_syn ("_\\_" [79, 1000] 76) and
+ flat ("|_|" [75] 74) and
+ flats ("|_|" [72] 74) and
+ Sequ ("_ @ _" [78,77] 63) and
+ injval ("inj _ _ _" [81,77,79] 76) and
+ mkeps ("mkeps _" [79] 76) and
+ length ("len _" [73] 73) and
+ intlen ("len _" [73] 73) and
+ set ("_" [73] 73) and
+
+ Prf ("_ : _" [75,75] 75) and
+ Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
+
+ lexer ("lexer _ _" [78,78] 77) and
+ DUMMY ("\<^latex>\<open>\\underline{\\hspace{2mm}}\<close>")
+*)
+(*>*)
+
+(*
+section {* Extensions*}
+
+text {*
+
+ A strong point in favour of
+ Sulzmann and Lu's algorithm is that it can be extended in various
+ ways. 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.
+
+ In the context of POSIX matching, it is also interesting to study additional
+ constructors about bounded-repetitions of regular expressions. For this let
+ us extend the results from the previous section to the following four
+ additional regular expression constructors:
+
+ \begin{center}
+ \begin{tabular}{lcrl@ {\hspace{12mm}}l}
+ @{text r} & @{text ":="} & $\ldots\mid$ & @{term "NTIMES r n"} & exactly-@{text n}-times\\
+ & & $\mid$ & @{term "UPNTIMES r n"} & upto-@{text n}-times\\
+ & & $\mid$ & @{term "FROMNTIMES r n"} & from-@{text n}-times\\
+ & & $\mid$ & @{term "NMTIMES r n m"} & between-@{text nm}-times\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ We will call them \emph{bounded regular expressions}.
+ With the help of the power operator (definition ommited) for sets of strings, the languages
+ recognised by these regular expression can be defined in Isabelle as follows:
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) L.simps(8)} & $\dn$ & @{thm (rhs) L.simps(8)}\\
+ @{thm (lhs) L.simps(7)} & $\dn$ & @{thm (rhs) L.simps(7)}\\
+ @{thm (lhs) L.simps(9)} & $\dn$ & @{thm (rhs) L.simps(9)}\\
+ @{thm (lhs) L.simps(10)} & $\dn$ & @{thm (rhs) L.simps(10)}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent This definition implies that in the last clause @{term
+ "NMTIMES r n m"} matches no string in case @{term "m < n"}, because
+ then the interval @{term "{n..m}"} is empty. While the language
+ recognised by these regular expressions is straightforward, some
+ care is needed for how to define the corresponding lexical
+ values. First, with a slight abuse of language, we will (re)use
+ values of the form @{term "Stars vs"} for values inhabited in
+ bounded regular expressions. Second, we need to introduce inductive
+ rules for extending our inhabitation relation shown on
+ Page~\ref{prfintros}, from which we then derived our notion of
+ lexical values. Given the rule for @{term "STAR r"}, the rule for
+ @{term "UPNTIMES r n"} just requires additionally that the length of
+ the list of values must be smaller or equal to @{term n}:
+
+ \begin{center}
+ @{thm[mode=Rule] Prf.intros(7)[of "vs"]}
+ \end{center}
+
+ \noindent Like in the @{term "STAR r"}-rule, we require with the
+ left-premise that some non-empty part of the string is `chipped'
+ away by \emph{every} value in @{text vs}, that means the corresponding
+ values do not flatten to the empty string. In the rule for @{term
+ "NTIMES r n"} (that is exactly-@{term n}-times @{text r}) we clearly need to require
+ that the length of the list of values equals to @{text n}. But enforcing
+ that every of these @{term n} values `chipps' away some part of a string
+ would be too strong.
+
+
+ \begin{center}
+ @{thm[mode=Rule] Prf.intros(8)[of "vs\<^sub>1" r "vs\<^sub>2"]}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) der.simps(8)} & $\dn$ & @{thm (rhs) der.simps(8)}\\
+ @{thm (lhs) der.simps(7)} & $\dn$ & @{thm (rhs) der.simps(7)}\\
+ @{thm (lhs) der.simps(9)} & $\dn$ & @{thm (rhs) der.simps(9)}\\
+ @{thm (lhs) der.simps(10)} & $\dn$ & @{thm (rhs) der.simps(10)}\\
+ \end{tabular}
+ \end{center}
+
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) mkeps.simps(5)} & $\dn$ & @{thm (rhs) mkeps.simps(5)}\\
+ @{thm (lhs) mkeps.simps(6)} & $\dn$ & @{thm (rhs) mkeps.simps(6)}\\
+ @{thm (lhs) mkeps.simps(7)} & $\dn$ & @{thm (rhs) mkeps.simps(7)}\\
+ @{thm (lhs) mkeps.simps(8)} & $\dn$ & @{thm (rhs) mkeps.simps(8)}\\
+ \end{tabular}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{lcl}
+ @{thm (lhs) injval.simps(8)} & $\dn$ & @{thm (rhs) injval.simps(8)}\\
+ @{thm (lhs) injval.simps(9)} & $\dn$ & @{thm (rhs) injval.simps(9)}\\
+ @{thm (lhs) injval.simps(10)} & $\dn$ & @{thm (rhs) injval.simps(10)}\\
+ @{thm (lhs) injval.simps(11)} & $\dn$ & @{thm (rhs) injval.simps(11)}\\
+ \end{tabular}
+ \end{center}
+
+
+ @{thm [mode=Rule] Posix_NTIMES1[of "s\<^sub>1" r v "s\<^sub>2"]}
+
+ @{thm [mode=Rule] Posix_NTIMES2}
+
+ @{thm [mode=Rule] Posix_UPNTIMES1[of "s\<^sub>1" r v "s\<^sub>2"]}
+
+ @{thm [mode=Rule] Posix_UPNTIMES2}
+
+ @{thm [mode=Rule] Posix_FROMNTIMES1[of "s\<^sub>1" r v "s\<^sub>2"]}
+
+ @{thm [mode=Rule] Posix_FROMNTIMES3[of "s\<^sub>1" r v "s\<^sub>2"]}
+
+ @{thm [mode=Rule] Posix_FROMNTIMES2}
+
+ @{thm [mode=Rule] Posix_NMTIMES1[of "s\<^sub>1" r v "s\<^sub>2"]}
+
+ @{thm [mode=Rule] Posix_NMTIMES3[of "s\<^sub>1" r v "s\<^sub>2"]}
+
+ @{thm [mode=Rule] Posix_NMTIMES2}
+
+
+
+ @{term "\<Sum> i \<in> {m..n} . P i"} @{term "\<Sum> i \<in> {..n} . P i"}
+ @{term "\<Union> i \<in> {m..n} . P i"} @{term "\<Union> i \<in> {..n} . P i"}
+ @{term "\<Union> i \<in> {0::nat..n} . P i"}
+
+
+
+*}
+
+
+
+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):
+
+ ??
+
+ \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.
+*}
+*)
+
+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 the Archive of Formal Proofs \cite{aduAFP16}
+ under \url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}.\medskip
+
+ \noindent
+ {\bf Acknowledgements:}
+ We are very grateful to Martin Sulzmann for his comments on our work and
+ moreover for 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
+(*>*)
\ No newline at end of file