# HG changeset patch # User Christian Urban # Date 1457421200 0 # Node ID f87e6e23bf179858b66aa7a9cbed9a0e95568d29 # Parent b208bc047eed07f4601e6fc5c509ec05d79d2869 updated diff -r b208bc047eed -r f87e6e23bf17 thys/Paper/Paper.thy --- 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. + *} diff -r b208bc047eed -r f87e6e23bf17 thys/paper.pdf Binary file thys/paper.pdf has changed