801 ONE"} to @{term r}. One of the advantages of having a simple specification |
804 ONE"} to @{term r}. One of the advantages of having a simple specification |
802 and correctness proof is that the latter can be refined to allow for such |
805 and correctness proof is that the latter can be refined to allow for such |
803 optimisations and simple correctness proof. |
806 optimisations and simple correctness proof. |
804 |
807 |
805 While the simplification of regular expressions according to |
808 While the simplification of regular expressions according to |
806 simplification rules |
809 rules like |
807 |
810 |
|
811 \begin{center} |
|
812 \begin{tabular}{lcl} |
|
813 @{term "ALT ZERO r"} & @{text "\<Rightarrow>"} & @{term r}\\ |
|
814 @{term "ALT r ZERO"} & @{text "\<Rightarrow>"} & @{term r}\\ |
|
815 @{term "SEQ ONE r"} & @{text "\<Rightarrow>"} & @{term r}\\ |
|
816 @{term "SEQ r ONE"} & @{text "\<Rightarrow>"} & @{term r} |
|
817 \end{tabular} |
|
818 \end{center} |
|
819 |
|
820 \noindent is well understood, there is an obstacle with the POSIX value |
|
821 calculation algorithm by Sulzmann and Lu: if we build a derivative regular |
|
822 expression and then simplify it, we will calculate a POSIX value for this |
|
823 simplified regular expression, \emph{not} for the original (unsimplified) |
|
824 derivative regular expression. Sulzmann and Lu overcome this obstacle by |
|
825 not just calculating a simplified regular expression, but also calculating |
|
826 a \emph{rectification function} that ``repairs'' the incorrect value. |
|
827 |
|
828 The rectification functions can be (slightly clumsily) implemented in |
|
829 Isabelle/HOL as follows using some auxiliary functions: |
|
830 |
|
831 \begin{center} |
|
832 \begin{tabular}{lcl} |
|
833 @{thm (lhs) F_RIGHT.simps(1)} & $\dn$ & @{text "Right (f v)"}\\ |
|
834 @{thm (lhs) F_LEFT.simps(1)} & $\dn$ & @{text "Left (f v)"}\\ |
|
835 |
|
836 @{thm (lhs) F_ALT.simps(1)} & $\dn$ & @{text "Right (f\<^sub>2 v)"}\\ |
|
837 @{thm (lhs) F_ALT.simps(2)} & $\dn$ & @{text "Left (f\<^sub>1 v)"}\\ |
|
838 |
|
839 @{thm (lhs) F_SEQ1.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 ()) (f\<^sub>2 v)"}\\ |
|
840 @{thm (lhs) F_SEQ2.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v) (f\<^sub>2 ())"}\\ |
|
841 @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}\bigskip\\ |
|
842 |
|
843 @{term "simp_ALT (ZERO, DUMMY) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_RIGHT f\<^sub>2)"}\\ |
|
844 @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, DUMMY)"} & $\dn$ & @{term "(r\<^sub>1, F_LEFT f\<^sub>1)"}\\ |
|
845 @{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)"}\\ |
|
846 @{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)"}\\ |
|
847 @{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)"}\\ |
|
848 @{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)"}\\ |
|
849 \end{tabular} |
|
850 \end{center} |
808 |
851 |
809 \noindent |
852 \noindent |
810 is well understood, there is a problem with the POSIX |
853 The main simplification function is then |
811 value calculation algorithm by Sulzmann and Lu: if we build a derivative |
854 |
812 regular expression and then simplify it, we will calculate a POSIX value |
855 \begin{center} |
813 for this simplified regular expression, \emph{not} for the original |
856 \begin{tabular}{lcl} |
814 (unsimplified) derivative regular expression. Sulzmann and Lu overcome |
857 @{term "simp (ALT r\<^sub>1 r\<^sub>2)"} & $\dn$ & @{term "simp_ALT (simp r\<^sub>1) (simp r\<^sub>2)"}\\ |
815 this problem by not just calculating a simplified regular expression, but |
858 @{term "simp (SEQ r\<^sub>1 r\<^sub>2)"} & $\dn$ & @{term "simp_SEQ (simp r\<^sub>1) (simp r\<^sub>2)"}\\ |
816 also calculating a \emph{rectification function} that ``repairs'' the |
859 @{term "simp r"} & $\dn$ & @{term "(r, id)"}\\ |
817 incorrect value. |
860 \end{tabular} |
|
861 \end{center} |
|
862 |
|
863 \noindent where @{term "id"} stands for the identity function. Note that |
|
864 we do not simplify under stars: this seems to slow down the algorithm, |
|
865 rather than speed up. The optimised lexer is then given by the clauses: |
|
866 |
|
867 \begin{center} |
|
868 \begin{tabular}{lcl} |
|
869 @{thm (lhs) matcher3.simps(1)} & $\dn$ & @{thm (rhs) matcher3.simps(1)}\\ |
|
870 @{thm (lhs) matcher3.simps(2)} & $\dn$ & |
|
871 @{text "let (r\<^sub>s, f\<^sub>r) = simp (r "}$\backslash$@{text " c) in"}\\ |
|
872 & & @{text "case"} @{term "matcher3 r\<^sub>s s"} @{text of}\\ |
|
873 & & \phantom{$|$} @{term "None"} @{text "\<Rightarrow>"} @{term None}\\ |
|
874 & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{text "Some (inj r c (f\<^sub>r v))"} |
|
875 \end{tabular} |
|
876 \end{center} |
|
877 |
|
878 \noindent |
|
879 In the second clause we first calculate the derivative @{text "r \\ c"} |
|
880 and then simplify the result. This gives us a simplified derivative |
|
881 @{text "r\<^sub>s"} and a rectification function @{text "f\<^sub>r"}. The matcher |
|
882 is recursively called with the simplified derivative, but before |
|
883 we inject the character @{term c} into value, we need to rectify |
|
884 it (@{term "f\<^sub>r v"}). We can prove that |
|
885 |
|
886 \begin{lemma} |
|
887 @{term "matcher3 r s = matcher r s"} |
|
888 \end{lemma} |
|
889 |
|
890 \noindent |
|
891 holds but refer the reader to our mechanisation for details. |
818 |
892 |
819 *} |
893 *} |
820 |
894 |
821 section {* The Argument by Sulzmmann and Lu *} |
895 section {* The Correctness Argument by Sulzmmann and Lu *} |
|
896 |
|
897 text {* |
|
898 \newcommand{\greedy}{\succcurlyeq_{gr}} |
|
899 \newcommand{\posix}{\succcurlyeq_{PX}} |
|
900 |
|
901 An extended version of \cite{Sulzmann2014} is available at the website of |
|
902 its first author; this includes some ``proofs'', claimed in |
|
903 \cite{Sulzmann2014} to be ``rigorous''. Since these are evidently not in |
|
904 final form, we make no comment thereon, preferring to give general reasons |
|
905 for our belief that the approach of \cite{Sulzmann2014} is problematic. |
|
906 |
|
907 Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch |
|
908 and Cardelli from where they have taken their main idea for their |
|
909 correctness proof of the POSIX algorithm. Frisch and Cardelli introduced |
|
910 an ordering, written $\greedy$, for values and they show that their greedy |
|
911 matching algorithm always produces a maximal element according to this |
|
912 ordering (from all possible solutions). The ordering $\greedy$ is defined |
|
913 by the following rules: |
|
914 |
|
915 \begin{center} |
|
916 \begin{tabular}{cc} |
|
917 \infer{v_{1} \greedy v'_{1}} {(v_{1},v_{2}) \greedy (v'_{1},v'_{2})} |
|
918 & |
|
919 \infer{v_{2} \greedy v'_{2}} {(v_{1},v_{2}) \greedy (v_{1},v'_{2})} |
|
920 \smallskip\\ |
|
921 \infer{v_{1} \greedy v_{2}} {Left \; v_{1} \greedy Left \; v_{2}} |
|
922 & |
|
923 \infer{v_{1} \greedy v_{2}} {Right \; v_{1} \greedy Right \; v_{2}} |
|
924 \\ |
|
925 |
|
926 \infer{\mbox{}}{Left \; v_{2}\greedy Right \; v_{1} } |
|
927 \medskip\\ |
|
928 |
|
929 $\infer{ v_{1} \greedy v_{2}} {v_{1} :: vs_{1} \greedy v_{2} :: vs_{2}} $ & |
|
930 $\infer{ vs_{1} \greedy vs_{2}} {v :: vs_{1} \greedy v :: vs_{2}}$ |
|
931 \\ |
|
932 |
|
933 & |
|
934 $\infer{\mbox{}} { v::vs \greedy []}$ |
|
935 \\ |
|
936 |
|
937 \infer{\mbox{}}{Char \; c \greedy Char \; c} |
|
938 & |
|
939 \infer{\mbox{}}{Void \greedy Void}\\ |
|
940 |
|
941 \end{tabular} |
|
942 \end{center} |
|
943 |
|
944 \noindent That these rules realise a greedy ordering can be |
|
945 seen in the first rule in the third line where a $Left$-value |
|
946 is always bigger than (or preferred over) a $Right$-value. |
|
947 What is interesting for our purposes is that the properties |
|
948 reflexivity, totality and transitivity for this greedy |
|
949 ordering can be proved relatively easily by |
|
950 induction. |
|
951 |
|
952 *} |
822 |
953 |
823 section {* Conclusion *} |
954 section {* Conclusion *} |
824 |
955 |
|
956 |
825 text {* |
957 text {* |
826 |
958 Nipkow lexer from 2000 |
827 Nipkow lexer from 2000 |
|
828 |
|
829 *} |
|
830 |
|
831 |
|
832 text {* |
|
833 |
|
834 |
959 |
835 \noindent |
960 \noindent |
836 We have also introduced a slightly restricted version of this relation |
961 We have also introduced a slightly restricted version of this relation |
837 where the last rule is restricted so that @{term "flat v \<noteq> []"}. |
962 where the last rule is restricted so that @{term "flat v \<noteq> []"}. |
838 \bigskip |
963 \bigskip |
839 |
964 |
840 |
965 |
841 \noindent |
|
842 |
|
843 |
|
844 \noindent |
|
845 Our version of Sulzmann's ordering relation |
|
846 |
|
847 |
|
848 *} |
|
849 |
|
850 text {* |
|
851 \noindent |
|
852 Some lemmas we have proved:\bigskip |
|
853 |
|
854 @{thm L_flat_Prf} |
|
855 |
|
856 @{thm[mode=IfThen] mkeps_nullable} |
|
857 |
|
858 @{thm[mode=IfThen] mkeps_flat} |
|
859 |
|
860 @{thm[mode=IfThen] Prf_injval} |
|
861 |
|
862 @{thm[mode=IfThen] Prf_injval_flat} |
|
863 |
|
864 @{thm[mode=IfThen] PMatch_mkeps} |
|
865 |
|
866 @{thm[mode=IfThen] PMatch1(2)} |
|
867 |
|
868 @{thm[mode=IfThen] PMatch_determ(1)[of "s" "r" "v\<^sub>1" "v\<^sub>2"]} |
|
869 |
|
870 |
|
871 \noindent {\bf Proof} The proof is by induction on the definition of |
|
872 @{const der}. Other inductions would go through as well. The |
|
873 interesting case is for @{term "SEQ r\<^sub>1 r\<^sub>2"}. First we analyse the |
|
874 case where @{term "nullable r\<^sub>1"}. We have by induction hypothesis |
|
875 |
|
876 \[ |
|
877 \begin{array}{l} |
|
878 (IH1)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>1 \<rightarrow> v"} |
|
879 \text{\;then\;} @{term "(c # s) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v"}\\ |
|
880 (IH2)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>2 \<rightarrow> v"} |
|
881 \text{\;then\;} @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> injval r\<^sub>2 c v"} |
|
882 \end{array} |
|
883 \] |
|
884 |
|
885 \noindent |
|
886 and have |
|
887 |
|
888 \[ |
|
889 @{term "s \<in> ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2) \<rightarrow> v"} |
|
890 \] |
|
891 |
|
892 \noindent |
|
893 There are two cases what @{term v} can be: (1) @{term "Left v'"} and (2) @{term "Right v'"}. |
|
894 |
|
895 \begin{itemize} |
|
896 \item[(1)] We know @{term "s \<in> SEQ (der c r\<^sub>1) r\<^sub>2 \<rightarrow> v'"} holds, from which we |
|
897 can infer that there are @{text "s\<^sub>1"}, @{term "s\<^sub>2"}, @{text "v\<^sub>1"}, @{term "v\<^sub>2"} |
|
898 with |
|
899 |
|
900 \[ |
|
901 @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} \qquad\text{and}\qquad @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} |
|
902 \] |
|
903 |
|
904 and also |
|
905 |
|
906 \[ |
|
907 @{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)"} |
|
908 \] |
|
909 |
|
910 \noindent |
|
911 and have to prove |
|
912 |
|
913 \[ |
|
914 @{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"} |
|
915 \] |
|
916 |
|
917 \noindent |
|
918 The two requirements @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"} and |
|
919 @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} can be proved by the induction hypothese (IH1) and the |
|
920 fact above. |
|
921 |
|
922 \noindent |
|
923 This leaves to prove |
|
924 |
|
925 \[ |
|
926 @{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)"} |
|
927 \] |
|
928 |
|
929 \noindent |
|
930 which holds because @{term "(c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 "} implies @{term "s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) "} |
|
931 |
|
932 \item[(2)] This case is similar. |
|
933 \end{itemize} |
|
934 |
|
935 \noindent |
|
936 The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar |
|
937 to the cases above. |
|
938 *} |
966 *} |
939 |
967 |
940 |
968 |
941 text {* |
969 text {* |
942 %\noindent |
970 %\noindent |