901 An extended version of \cite{Sulzmann2014} is available at the website of |
901 An extended version of \cite{Sulzmann2014} is available at the website of |
902 its first author; this includes some ``proofs'', claimed in |
902 its first author; this includes some ``proofs'', claimed in |
903 \cite{Sulzmann2014} to be ``rigorous''. Since these are evidently not 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 |
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. |
905 for our belief that the approach of \cite{Sulzmann2014} is problematic. |
906 Their central definition is an ``ordering relation'' |
906 Their central definition is an ``ordering relation'' defined by the |
|
907 rules (slightly adapted to fit our notation): |
907 |
908 |
908 \begin{center} |
909 \begin{center} |
909 \begin{tabular}{c@ {\hspace{5mm}}c} |
910 \begin{tabular}{@ {}c@ {\hspace{2mm}}c@ {}} |
910 $\infer{v_{1} \posix_{r_{1}} v'_{1}} |
911 $\infer{v_{1} \posix_{r_{1}} v'_{1}} |
911 {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v'_{1}\,v'_{2}}(C2)$ |
912 {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v'_{1}\,v'_{2}}(C2)$ |
912 & |
913 & |
913 $\infer{v_{2} \posix_{r_{2}} v'_{2}} |
914 $\infer{v_{2} \posix_{r_{2}} v'_{2}} |
914 {Seq\,v_{1}\,v_{2}) \posix_{r_{1}r_{2}} Seq\,v_{1}\,v'_{2}}(C1)$ |
915 {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v_{1}\,v'_{2}}(C1)$ |
915 \medskip\\ |
916 \medskip\\ |
916 |
917 |
917 |
918 |
918 $\infer{ len |v_{2}| > len |v_{1}|} |
919 $\infer{ len |v_{2}| > len |v_{1}|} |
919 {Right \; v_{2} \posix_{r_{1}+r_{2}} Left \; v_{1}}(A1)$ |
920 {Right \; v_{2} \posix_{r_{1}+r_{2}} Left \; v_{1}}(A1)$ |
927 |
928 |
928 $\infer{ v_{1} \posix_{r_{1}} v'_{1}} |
929 $\infer{ v_{1} \posix_{r_{1}} v'_{1}} |
929 {Left \; v_{1} \posix_{r_{1}+r_{2}} Left \; v'_{1}}(A4)$ |
930 {Left \; v_{1} \posix_{r_{1}+r_{2}} Left \; v'_{1}}(A4)$ |
930 \medskip\\ |
931 \medskip\\ |
931 |
932 |
932 $\infer{|v :: vs| = []} {[] \posix_{r^{\star}} v :: vs}(K1)$ & |
933 $\infer{|v :: vs| = []} {Stars\,[] \posix_{r^{\star}} Stars\,(v :: vs)}(K1)$ & |
933 $\infer{|v :: vs| \neq []} { v :: vs \posix_{r^{\star}} []}(K2)$ |
934 $\infer{|v :: vs| \neq []} {Stars\,(v :: vs) \posix_{r^{\star}} Stars\,[]}(K2)$ |
934 \medskip\\ |
935 \medskip\\ |
935 |
936 |
936 $\infer{ v_{1} \posix_{r} v_{2}} |
937 $\infer{ v_{1} \posix_{r} v_{2}} |
937 {v_{1} :: vs_{1} \posix_{r^{\star}} v_{2} :: vs_{2}}(K3)$ & |
938 {Stars\,(v_{1} :: vs_{1}) \posix_{r^{\star}} Stars\,(v_{2} :: vs_{2})}(K3)$ & |
938 $\infer{ vs_{1} \posix_{r^{\star}} vs_{2}} |
939 $\infer{ Stars\,vs_{1} \posix_{r^{\star}} Stars\,vs_{2}} |
939 {v :: vs_{1} \posix_{r^{\star}} v :: vs_{2}}(K4)$ |
940 {Stars\,(v :: vs_{1}) \posix_{r^{\star}} Stars\,(v :: vs_{2})}(K4)$ |
940 \end{tabular} |
941 \end{tabular} |
941 \end{center} |
942 \end{center} |
942 |
943 |
943 Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch |
944 Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch |
944 and Cardelli from where they have taken their main idea for their |
945 and Cardelli from where they have taken their main idea for their |