944 {Stars\,(v :: vs_{1}) \posix_{r^{\star}} Stars\,(v :: vs_{2})}(K4)$ |
944 {Stars\,(v :: vs_{1}) \posix_{r^{\star}} Stars\,(v :: vs_{2})}(K4)$ |
945 \end{tabular} |
945 \end{tabular} |
946 \end{center} |
946 \end{center} |
947 |
947 |
948 \noindent |
948 \noindent |
949 The idea behind the rules $(A1)$ and $(A2)$ is that a $Left$-value is |
949 The idea behind the rules $(A1)$ and $(A2)$, for example, is that a $Left$-value is |
950 bigger than a $Right$-value, if the underlying string of the $Left$-value is |
950 bigger than a $Right$-value, if the underlying string of the $Left$-value is |
951 bigger or equals to the underlying string of the $Right$-value. The order |
951 longer or of equal length to the underlying string of the $Right$-value. The order |
952 is reversed if the $Right$-value can match longer string than a $Left$-value. |
952 is reversed, however, if the $Right$-value can match longer string than a $Left$-value. |
953 In this way the POSIX value is supposed to be the biggest value |
953 In this way the POSIX value is supposed to be the biggest value |
954 for a given string and regular expression. |
954 for a given string and regular expression. |
955 |
955 |
956 Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch |
956 Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch |
957 and Cardelli from where they have taken the idea for their correctness |
957 and Cardelli from where they have taken the idea for their correctness |
958 proof of the POSIX value algorithm. Frisch and Cardelli introduced a |
958 proof. Frisch and Cardelli introduced a |
959 similar ordering for GREEDY matching and they show that their greedy |
959 similar ordering for GREEDY matching and they show that their GREEDY |
960 matching algorithm always produces a maximal element according to this |
960 matching algorithm always produces a maximal element according to this |
961 ordering (from all possible solutions). The only difference between their |
961 ordering (from all possible solutions). The only difference between their |
962 GREEDY ordering and the ``ordering'' by Sulzmann and Lu is that GREEDY, if |
962 GREEDY ordering and the ``ordering'' by Sulzmann and Lu is that GREEDY, if |
963 possible, always prefers a $Left$-value over a $Right$-value, no matter |
963 possible, always prefers a $Left$-value over a $Right$-value, no matter |
964 what the underlying string is. This seems like only a very minor |
964 what the underlying string is. This seems like only a very minor |