1030 \begin{center} |
1030 \begin{center} |
1031 \begin{tabular}{@ {}cc@ {}} |
1031 \begin{tabular}{@ {}cc@ {}} |
1032 \begin{tabular}{@ {}ll@ {}} |
1032 \begin{tabular}{@ {}ll@ {}} |
1033 IH $r_1$:\\ |
1033 IH $r_1$:\\ |
1034 $\forall v_1, v_2, v_3.$ |
1034 $\forall v_1, v_2, v_3.$ |
1035 & $v_1 : r_1\;\wedge$\\ |
1035 & $v_1 : r_1\;\wedge$ |
1036 & $v_2 : r_1\;\wedge$\\ |
1036 $v_2 : r_1\;\wedge$ |
1037 & $v_3 : r_1\;\wedge$\\ |
1037 $v_3 : r_1\;\wedge$\\ |
1038 & $|v_1|=|v_2|=|v_3|\;\wedge$\\ |
1038 & $|v_1|=|v_2|=|v_3|\;\wedge$\\ |
1039 & $v_1 \posix_{r_1} v_2\;\wedge\; v_2 \posix_{r_1} v_3$\medskip\\ |
1039 & $v_1 \posix_{r_1} v_2\;\wedge\; v_2 \posix_{r_1} v_3$\medskip\\ |
1040 & $\;\;\Rightarrow v_1 \posix_{r_1} v_3$ |
1040 & $\;\;\Rightarrow v_1 \posix_{r_1} v_3$ |
1041 \end{tabular} & |
1041 \end{tabular} & |
1042 \begin{tabular}{@ {}ll@ {}} |
1042 \begin{tabular}{@ {}ll@ {}} |
1043 IH $r_2$:\\ |
1043 IH $r_2$:\\ |
1044 $\forall v_1, v_2, v_3.$ |
1044 $\forall v_1, v_2, v_3.$ |
1045 & $v_1 : r_2\;\wedge$\\ |
1045 & $v_1 : r_2\;\wedge$ |
1046 & $v_2 : r_2\;\wedge$\\ |
1046 $v_2 : r_2\;\wedge$ |
1047 & $v_3 : r_2\;\wedge$\\ |
1047 $v_3 : r_2\;\wedge$\\ |
1048 & $|v_1|=|v_2|=|v_3|\;\wedge$\\ |
1048 & $|v_1|=|v_2|=|v_3|\;\wedge$\\ |
1049 & $v_1 \posix_{r_2} v_2\;\wedge\; v_2 \posix_{r_2} v_3$\medskip\\ |
1049 & $v_1 \posix_{r_2} v_2\;\wedge\; v_2 \posix_{r_2} v_3$\medskip\\ |
1050 & $\;\;\Rightarrow v_1 \posix_{r_2} v_3$ |
1050 & $\;\;\Rightarrow v_1 \posix_{r_2} v_3$ |
1051 \end{tabular} |
1051 \end{tabular} |
1052 \end{tabular} |
1052 \end{tabular} |
1071 \qquad\textrm{and}\qquad |
1071 \qquad\textrm{and}\qquad |
1072 |Seq\,v_{2l}\, v_{2r}| = |Seq\,v_{3l}\, v_{3r}| |
1072 |Seq\,v_{2l}\, v_{2r}| = |Seq\,v_{3l}\, v_{3r}| |
1073 \label{lens} |
1073 \label{lens} |
1074 \end{equation} |
1074 \end{equation} |
1075 |
1075 |
1076 \noindent |
1076 \noindent We need to show that $Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2} |
1077 We need to show that |
1077 Seq\, v_{3l}\, v_{3r}$ holds. We can proceed by analysing how the |
1078 |
1078 assumptions in \eqref{assms} have arisen. There are four cases. Let us |
1079 \[ |
1079 assume we are in the case where we know |
1080 Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2} Seq\, v_{3l}\, v_{3r} |
|
1081 \] |
|
1082 |
|
1083 \noindent holds. We can proceed by analysing how the |
|
1084 assumptions in \eqref{assms} have arisen. There are four |
|
1085 cases. Let us assume we are in the case where |
|
1086 we know |
|
1087 |
1080 |
1088 \[ |
1081 \[ |
1089 v_{1l} \posix_{r_1} v_{2l} |
1082 v_{1l} \posix_{r_1} v_{2l} |
1090 \qquad\textrm{and}\qquad |
1083 \qquad\textrm{and}\qquad |
1091 v_{2l} \posix_{r_1} v_{3l} |
1084 v_{2l} \posix_{r_1} v_{3l} |
1128 by Sulzmann and Lu \cite{Sulzmann2014}, but we believe it contains |
1121 by Sulzmann and Lu \cite{Sulzmann2014}, but we believe it contains |
1129 unfillable gaps. In the online version of \cite{Sulzmann2014}, the authors |
1122 unfillable gaps. In the online version of \cite{Sulzmann2014}, the authors |
1130 already acknowledge some small problems, but our experience suggests |
1123 already acknowledge some small problems, but our experience suggests |
1131 that there are more serious problems. |
1124 that there are more serious problems. |
1132 |
1125 |
|
1126 Having proved the correctness of the POSIX lexing algorithm in |
|
1127 \cite{Sulzmann2014}, which lessons have we learned? Well, this is a |
|
1128 perfect example for the importance of the \emph{right} definitions. We |
|
1129 have (on and off) banged our heads on doors as soon as as first versions |
|
1130 of \cite{Sulzmann2014} appeared, but have made little progress with |
|
1131 turning the relatively detailed proof sketch in \cite{Sulzmann2014} into a |
|
1132 formalisable proof. Having seen \cite{Vansummeren2006} and adapting the |
|
1133 POSIX definition given there for the algorithm by Sulzmann and Lu made all |
|
1134 the difference: the proofs, as said, are nearly straightforward. The |
|
1135 question remains whether the original proof idea of \cite{Sulzmann2014}, |
|
1136 potentially using our result as a stepping stone, can be made to work? |
|
1137 Alas, we really do not know despite considerable effort and door banging. |
|
1138 |
|
1139 |
1133 Closely related to our work is an automata-based lexer formalised by |
1140 Closely related to our work is an automata-based lexer formalised by |
1134 Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest |
1141 Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest |
1135 initial substrings, but Nipkow's algorithm is not completely |
1142 initial substrings, but Nipkow's algorithm is not completely |
1136 computational. The algorithm by Sulzmann and Lu, in contrast, can be |
1143 computational. The algorithm by Sulzmann and Lu, in contrast, can be |
1137 implemented with easy in any functional language. A bespoke lexer for the |
1144 implemented with easy in any functional language. A bespoke lexer for the |