lexing: comparison thys/Paper/Paper.thy

equal deleted inserted replaced

-:f28cf86a1e7f
+:a05b3c89e8aa
 similar ordering for GREEDY matching and they show that their GREEDY
 matching algorithm always produces a maximal element according to this
 ordering (from all possible solutions). The only difference between their
 GREEDY ordering and the ``ordering'' by Sulzmann and Lu is that GREEDY, if
 possible, always prefers a $Left$-value over a $Right$-value, no matter
-what the underlying string is. This seems like only a very minor
+what the underlying string is. This seems to be only a very minor
-difference, but it leads to drastic consequences in terms what
+difference, but it has drastic consequences in terms of what
 properties both orderings enjoy. What is interesting for our purposes is
 that the properties reflexivity, totality and transitivity for this GREEDY
 ordering can be proved relatively easily by induction.
 These properties of GREEDY, however, do not transfer to the POSIX
-``ordering'' by Sulzmann and Lu. To start with, $v \geq_r v′$ is not
+``ordering'' by Sulzmann and Lu. To start with, $v \geq_r v'$ is not
-defined inductively, but as $v = v′$ or $v >_r v′ \wedge |v| = |v′|$. This
+defined inductively, but as $v = v'$ or $v >_r v' \wedge |v| = |v'|$. This
-means that $v >_r v′$ does not imply $v \geq_r v′$. Moreover, transitivity
+means that $v >_r v'$ does not imply $v \geq_r v'$. Moreover, transitivity
 does not hold in the ``usual'' formulation, for example:
 \begin{proposition}
 Suppose $v_1 : r$, $v_2 : r$ and $v_3 : r$.
 If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$
 then $v_1 \posix_r v_3$.
 \end{proposition}
-\noindent If formulated like this, then there are various counter examples:
+\noindent If formulated in this way, then there are various counter examples:
-FOr example let $r$ be $a + ((a + a)\cdot (a + \textbf{0}))$ then the $v_1$,
+For example let $r$ be $a + ((a + a)\cdot (a + \textbf{0}))$ then the $v_1$,
 $v_2$ and $v_3$ below are values of $r$:
 \begin{center}
 \begin{tabular}{lcl}
 $v_1$ & $=$ & $Left(Char\;a)$\\
-$v_2$ & $=$ & $Right((Left(Char\;a), Right(Void)))$\\
+$v_2$ & $=$ & $Right((Left(Char\;a), Right()))$\\
 $v_3$ & $=$ & $Right((Right(Char\;a), Left(Char\;a)))$
 \end{tabular}
 \end{center}
 \noindent Moreover $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$,
 but \emph{not} $v_1 \posix_r v_3$! The reason is that although
 $v_3$ is a $Right$-value, it can match a longer string, namely
-$|v_3| = aa$, while $|v_1|$ (and $|v_2|$) matches only $a$. So
+$|v_3| = [a,a]$, while $|v_1|$ (and $|v_2|$) matches only $[a]$. So
 transitivity in this formulation does not hold---in this
 example actually $v_3 \posix_r v_1$!
 Sulzmann and Lu ``fix'' this problem by weakening the
 transitivity property. They require in addition that the
 underlying strings are of the same length. This excludes the
 counter example above and any counter-example we were able
 to find (by hand and by machine). Thus the transitivity
-lemma in should be formulated as:
+lemma should be formulated as:
-\begin{property}
+\begin{proposition}
 Suppose $v_1 : r$, $v_2 : r$ and
 $v_3 : r$, and also $|v_1|=|v_2|=|v_3|$.\\
 If $v_1 \posix_r v_2$ and $v_2 \posix_r v_3$
 then $v_1 \posix_r v_3$.
-\end{property}
+\end{proposition}
-\noindent While we agree with Sulzmann and Lu that this property probably
+\noindent While we agree with Sulzmann and Lu that this property probably(!)
 holds, proving it seems not so straightforward: although one begins with the
 assumption that the values have the same flattening, this
 cannot be maintained as one descends into the induction. This is
-a problem that occurs in a number of places in their proof.
+a problem that occurs in a number of places in the proofs by Sulzmann and Lu.
-Sulzmann and Lu do not give an explicit proof
-of the transitivity property, but give a closely related
+Although they do not give an explicit proof
+of the transitivity property, they give a closely related
 property about the existence of maximal elements. They state
 that this can be verified by an induction on $r$. We disagree
 with this as we shall show next in case of transitivity.
 The case where the reasoning breaks down is the sequence case,
 say $r_1\cdot r_2$. The induction hypotheses in this case
 are
 \begin{center}
 \noindent
 hold, and furthermore that the values have equal length,
 namely:
 \begin{equation}
-|(v_{1l}, v_{1r})| = |(v_{2l}, v_{2r})|
+|Seq\,v_{1l}\, v_{1r}| = |Seq\,v_{2l}\, v_{2r}|
 \qquad\textrm{and}\qquad
-|(v_{2l}, v_{2r})| = |(v_{3l}, v_{3r})|
+|Seq\,v_{2l}\, v_{2r}| = |Seq\,v_{3l}\, v_{3r}|
 \label{lens}
 \end{equation}
 \noindent
 We need to show that
 \[
-Seq\,v_{1l}\, v_{1r}) \posix_{r_1\cdot r_2} Seq\, v_{3l}\, v_{3r}
+Seq\,v_{1l}\, v_{1r} \posix_{r_1\cdot r_2} Seq\, v_{3l}\, v_{3r}
 \]
 \noindent holds. We can proceed by analysing how the
 assumptions in \eqref{assms} have arisen. There are four
 cases. Let us assume we are in the case where
 \]
 \noindent but still \eqref{lens} will hold. Now we are stuck,
 since the IH does not apply. As said, this problem where the
 induction hypothesis does not apply arises in several places in
-the proof of Sulzmann and LU, not just when proving transitivity.
+the proof of Sulzmann and Lu, not just for proving transitivity.
 *}
 section {* Conclusion *}

changeset 140	a05b3c89e8aa
parent 139	f28cf86a1e7f
child 141	879d43256063