443 there are several ways). This function is defined by the clauses: |
443 there are several ways). This function is defined by the clauses: |
444 |
444 |
445 \begin{figure}[t] |
445 \begin{figure}[t] |
446 \begin{center} |
446 \begin{center} |
447 \begin{tikzpicture}[scale=2,node distance=1.3cm, |
447 \begin{tikzpicture}[scale=2,node distance=1.3cm, |
448 every node/.style={minimum size=7mm}] |
448 every node/.style={minimum size=6mm}] |
449 \node (r1) {@{term "r\<^sub>1"}}; |
449 \node (r1) {@{term "r\<^sub>1"}}; |
450 \node (r2) [right=of r1]{@{term "r\<^sub>2"}}; |
450 \node (r2) [right=of r1]{@{term "r\<^sub>2"}}; |
451 \draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}}; |
451 \draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}}; |
452 \node (r3) [right=of r2]{@{term "r\<^sub>3"}}; |
452 \node (r3) [right=of r2]{@{term "r\<^sub>3"}}; |
453 \draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}}; |
453 \draw[->,line width=1mm](r2)--(r3) node[above,midway] {@{term "der b DUMMY"}}; |
463 \node (v1) [left=of v2] {@{term "v\<^sub>1"}}; |
463 \node (v1) [left=of v2] {@{term "v\<^sub>1"}}; |
464 \draw[->,line width=1mm](v2)--(v1) node[below,midway] {@{text "inj r\<^sub>1 a"}}; |
464 \draw[->,line width=1mm](v2)--(v1) node[below,midway] {@{text "inj r\<^sub>1 a"}}; |
465 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}}; |
465 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}}; |
466 \end{tikzpicture} |
466 \end{tikzpicture} |
467 \end{center} |
467 \end{center} |
|
468 \mbox{}\\[-13mm] |
|
469 |
468 \caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014}, |
470 \caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014}, |
469 matching the string @{term "[a,b,c]"}. The first phase (the arrows from |
471 matching the string @{term "[a,b,c]"}. The first phase (the arrows from |
470 left to right) is \Brz's matcher building successive derivatives. If the |
472 left to right) is \Brz's matcher building successive derivatives. If the |
471 last regular expression is @{term nullable}, then the functions of the |
473 last regular expression is @{term nullable}, then the functions of the |
472 second phase are called (the top-down and right-to-left arrows): first |
474 second phase are called (the top-down and right-to-left arrows): first |
1206 that there are more serious problems. |
1208 that there are more serious problems. |
1207 |
1209 |
1208 Having proved the correctness of the POSIX lexing algorithm in |
1210 Having proved the correctness of the POSIX lexing algorithm in |
1209 \cite{Sulzmann2014}, which lessons have we learned? Well, this is a |
1211 \cite{Sulzmann2014}, which lessons have we learned? Well, this is a |
1210 perfect example for the importance of the \emph{right} definitions. We |
1212 perfect example for the importance of the \emph{right} definitions. We |
1211 have (on and off) banged our heads on doors as soon as first versions |
1213 have (on and off) explored mechanisations as soon as first versions |
1212 of \cite{Sulzmann2014} appeared, but have made little progress with |
1214 of \cite{Sulzmann2014} appeared, but have made little progress with |
1213 turning the relatively detailed proof sketch in \cite{Sulzmann2014} into a |
1215 turning the relatively detailed proof sketch in \cite{Sulzmann2014} into a |
1214 formalisable proof. Having seen \cite{Vansummeren2006} and adapted the |
1216 formalisable proof. Having seen \cite{Vansummeren2006} and adapted the |
1215 POSIX definition given there for the algorithm by Sulzmann and Lu made all |
1217 POSIX definition given there for the algorithm by Sulzmann and Lu made all |
1216 the difference: the proofs, as said, are nearly straightforward. The |
1218 the difference: the proofs, as said, are nearly straightforward. The |
1217 question remains whether the original proof idea of \cite{Sulzmann2014}, |
1219 question remains whether the original proof idea of \cite{Sulzmann2014}, |
1218 potentially using our result as a stepping stone, can be made to work? |
1220 potentially using our result as a stepping stone, can be made to work? |
1219 Alas, we really do not know despite considerable effort and door banging. |
1221 Alas, we really do not know despite considerable effort. |
1220 |
1222 |
1221 |
1223 |
1222 Closely related to our work is an automata-based lexer formalised by |
1224 Closely related to our work is an automata-based lexer formalised by |
1223 Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest |
1225 Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest |
1224 initial substrings, but Nipkow's algorithm is not completely |
1226 initial substrings, but Nipkow's algorithm is not completely |