--- a/thys/Paper/Paper.thy Tue Mar 08 06:30:48 2016 +0000
+++ b/thys/Paper/Paper.thy Tue Mar 08 07:13:20 2016 +0000
@@ -896,58 +896,201 @@
text {*
\newcommand{\greedy}{\succcurlyeq_{gr}}
- \newcommand{\posix}{\succcurlyeq_{PX}}
+ \newcommand{\posix}{>}
An extended version of \cite{Sulzmann2014} is available at the website of
its first author; this includes some ``proofs'', claimed in
\cite{Sulzmann2014} to be ``rigorous''. Since these are evidently not in
final form, we make no comment thereon, preferring to give general reasons
for our belief that the approach of \cite{Sulzmann2014} is problematic.
+ Their central definition is an ``ordering relation''
+
+\begin{center}
+\begin{tabular}{c@ {\hspace{5mm}}c}
+$\infer{v_{1} \posix_{r_{1}} v'_{1}}
+ {Seq\,v_{1}\,v_{2} \posix_{r_{1}r_{2}} Seq\,v'_{1}\,v'_{2}}(C2)$
+&
+$\infer{v_{2} \posix_{r_{2}} v'_{2}}
+ {Seq\,v_{1}\,v_{2}) \posix_{r_{1}r_{2}} Seq\,v_{1}\,v'_{2}}(C1)$
+\medskip\\
+
+
+$\infer{ len |v_{2}| > len |v_{1}|}
+ {Right \; v_{2} \posix_{r_{1}+r_{2}} Left \; v_{1}}(A1)$
+&
+$\infer{ len |v_{1}| \geq len |v_{2}|}
+ {Left \; v_{1} \posix_{r_{1}+r_{2}} Right \; v_{2}} (A2)$
+\medskip\\
+
+$\infer{ v_{2} \posix_{r_{2}} v'_{2}}
+ {Right \; v_{2} \posix_{r_{1}+r_{2}} Right \; v'_{2}}(A3)$ &
+
+$\infer{ v_{1} \posix_{r_{1}} v'_{1}}
+ {Left \; v_{1} \posix_{r_{1}+r_{2}} Left \; v'_{1}}(A4)$
+\medskip\\
+
+ $\infer{|v :: vs| = []} {[] \posix_{r^{\star}} v :: vs}(K1)$ &
+ $\infer{|v :: vs| \neq []} { v :: vs \posix_{r^{\star}} []}(K2)$
+\medskip\\
+
+$\infer{ v_{1} \posix_{r} v_{2}}
+ {v_{1} :: vs_{1} \posix_{r^{\star}} v_{2} :: vs_{2}}(K3)$ &
+$\infer{ vs_{1} \posix_{r^{\star}} vs_{2}}
+ {v :: vs_{1} \posix_{r^{\star}} v :: vs_{2}}(K4)$
+\end{tabular}
+\end{center}
Sulzmann and Lu explicitly refer to the paper \cite{Frisch2004} by Frisch
and Cardelli from where they have taken their main idea for their
- correctness proof of the POSIX algorithm. Frisch and Cardelli introduced
- an ordering, written $\greedy$, for values and they show that their greedy
- matching algorithm always produces a maximal element according to this
- ordering (from all possible solutions). The ordering $\greedy$ is defined
- by the following rules:
+ correctness proof of the POSIX value algorithm. Frisch and Cardelli
+ introduced an ordering, written $\greedy$, for values 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 always prefers a $Left$-value over a $Right-value$.
+ 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 POSIX by
+ Sulzmann and Lu. To start with, transitivity does not hold anymore in the
+``normal'' formulation, that is:
+
+\begin{property}
+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{property}
+
+\noindent If formulated like this, then there are various counter examples:
+Suppose $r$ is $a + ((a + a)(a + \textbf{0}))$ then the $v_1$, $v_2$ and $v_3$
+below are values of $r$:
\begin{center}
-\begin{tabular}{cc}
-\infer{v_{1} \greedy v'_{1}} {(v_{1},v_{2}) \greedy (v'_{1},v'_{2})}
-&
-\infer{v_{2} \greedy v'_{2}} {(v_{1},v_{2}) \greedy (v_{1},v'_{2})}
-\smallskip\\
-\infer{v_{1} \greedy v_{2}} {Left \; v_{1} \greedy Left \; v_{2}}
-&
-\infer{v_{1} \greedy v_{2}} {Right \; v_{1} \greedy Right \; v_{2}}
-\\
-
-\infer{\mbox{}}{Left \; v_{2}\greedy Right \; v_{1} }
-\medskip\\
-
-$\infer{ v_{1} \greedy v_{2}} {v_{1} :: vs_{1} \greedy v_{2} :: vs_{2}} $ &
-$\infer{ vs_{1} \greedy vs_{2}} {v :: vs_{1} \greedy v :: vs_{2}}$
-\\
-
-&
-$\infer{\mbox{}} { v::vs \greedy []}$
-\\
-
-\infer{\mbox{}}{Char \; c \greedy Char \; c}
-&
-\infer{\mbox{}}{Void \greedy Void}\\
-
+\begin{tabular}{lcl}
+ $v_1$ & $=$ & $Left(Char\;a)$\\
+ $v_2$ & $=$ & $Right((Left(Char\;a), Right(Void)))$\\
+ $v_3$ & $=$ & $Right((Right(Char\;a), Left(Char\;a)))$
\end{tabular}
\end{center}
-\noindent That these rules realise a greedy ordering can be
-seen in the first rule in the third line where a $Left$-value
-is always bigger than (or preferred over) a $Right$-value.
-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.
+\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
+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 could find
+with our implementation. Thus the transitivity lemma in
+\cite{Sulzmann2014} is:
+
+\begin{property}
+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}
+
+\noindent While we agree with Sulzmann and Lu that this
+property probably holds, proving it seems not so
+straightforward. Sulzmann and Lu do not give an explicit proof
+of the transitivity property, but 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\,r_2$. The induction hypotheses in this case
+are
+
+\begin{center}
+\begin{tabular}{@ {}cc@ {}}
+\begin{tabular}{@ {}ll@ {}}
+IH $r_1$:\\
+$\forall v_1, v_2, v_3.$
+ & $\vdash v_1 : r_1\;\wedge$\\
+ & $\vdash v_2 : r_1\;\wedge$\\
+ & $\vdash v_3 : r_1\;\wedge$\\
+ & $|v_1|=|v_2|=|v_3|\;\wedge$\\
+ & $v_1 \posix^{r_1} v_2\;\wedge\; v_2 \posix^{r_1} v_3$\medskip\\
+ & $\;\;\Rightarrow v_1 \posix^{r_1} v_3$
+\end{tabular} &
+\begin{tabular}{@ {}ll@ {}}
+IH $r_2$:\\
+$\forall v_1, v_2, v_3.$
+ & $\vdash v_1 : r_2\;\wedge$\\
+ & $\vdash v_2 : r_2\;\wedge$\\
+ & $\vdash v_3 : r_2\;\wedge$\\
+ & $|v_1|=|v_2|=|v_3|\;\wedge$\\
+ & $v_1 \posix^{r_2} v_2\;\wedge\; v_2 \posix^{r_2} v_3$\medskip\\
+ & $\;\;\Rightarrow v_1 \posix^{r_2} v_3$
+\end{tabular}
+\end{tabular}
+\end{center}
+
+\noindent
+We can assume that
+
+\begin{equation}
+(v_{1l}, v_{1r}) \posix^{r_1\,r_2} (v_{2l}, v_{2r})
+\qquad\textrm{and}\qquad
+(v_{2l}, v_{2r}) \posix^{r_1\,r_2} (v_{3l}, v_{3r})
+\label{assms}
+\end{equation}
+
+\noindent
+hold, and furthermore that the values have equal length,
+namely:
+
+\begin{equation}
+|(v_{1l}, v_{1r})| = |(v_{2l}, v_{2r})|
+\qquad\textrm{and}\qquad
+|(v_{2l}, v_{2r})| = |(v_{3l}, v_{3r})|
+\label{lens}
+\end{equation}
+
+\noindent
+We need to show that
+
+\[
+(v_{1l}, v_{1r}) \posix^{r_1\,r_2} (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
+we know
+
+\[
+v_{1l} \posix^{r_1} v_{2l}
+\qquad\textrm{and}\qquad
+v_{2l} \posix^{r_1} v_{3l}
+\]
+
+\noindent and also know the corresponding typing judgements.
+This is exactly a case where we would like to apply the
+induction hypothesis IH~$r_1$. But we cannot! We still need to
+show that $|v_{1l}| = |v_{2l}|$ and $|v_{2l}| = |v_{3l}|$. We
+know from \eqref{lens} that the lengths of the sequence values
+are equal, but from this we cannot infer anything about the
+lengths of the component values. Indeed in general they will
+be unequal, that is
+
+\[
+|v_{1l}| \not= |v_{2l}|
+\qquad\textrm{and}\qquad
+|v_{1r}| \not= |v_{2r}|
+\]
+
+\noindent but still \eqref{lens} will hold. Now we are stuck,
+since the IH does not apply. Sulzmann and Lu overlook this
+fact and just apply the IHs. Obviously nothing which a
+theorem prover allows us to do.
+
*}