lemmas.tex

   1 \section{Some lemmas}
   2
   3 \subsection{Alternative (overlapping) formulations of $\mergeof{C}{L}{M}{R}$}
   4 $$
   5  D \isin C \equiv
   6   \begin{cases}
   7     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
   8     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
   9     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
  10     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
  11     \text{as above with L and R exchanged}
  12   \end{cases}
  13 $$
  14 \proof{ ~ Truth table (ordered by original definition): \\
  15   \begin{tabular}{cccc|c|cc}
  16      $D = C$ &
  17           $\isin L$ &
  18                $\isin M$ &
  19                     $\isin R$ & $\isin C$ &
  20                                       $L$ vs. $R$ & $L$ vs. $M$
  21   \\\hline
  22      y &  ? &  ? &  ?      &      y   & ?         & ?            \\
  23      n &  y &  y &  y      &      y   & $\equiv$  & $\equiv$     \\
  24      n &  y &  n &  y      &      y   & $\equiv$  & $\nequiv$    \\
  25      n &  n &  y &  n      &      n   & $\equiv$  & $\nequiv$    \\
  26      n &  n &  n &  n      &      n   & $\equiv$  & $\equiv$     \\
  27      n &  y &  y &  n      &      n   & $\nequiv$ & $\equiv$     \\
  28      n &  n &  y &  y      &      n   & $\nequiv$ & $\nequiv$    \\
  29      n &  y &  n &  n      &      y   & $\nequiv$ & $\nequiv$    \\
  30      n &  n &  n &  y      &      y   & $\nequiv$ & $\equiv$     \\
  31   \end{tabular} \\
  32   And original definition is symmetrical in $L$ and $R$.
  33 }
  34
  35 \subsection{Exclusive Tip Contents}
  36 Given Base Acyclic for $C$,
  37 $$
  38   \bigforall_{C \in \py}
  39     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
  40       \Bigr]
  41 $$
  42 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
  43
  44 \proof{
  45 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
  46 So by Base Acyclic $D \isin B \implies D \notin \py$.
  47 }
  48 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
  49   \bigforall_{C \in \py} D \isin C \equiv
  50   \begin{cases}
  51     D \in \py : & D \le C \\
  52     D \not\in \py : & D \isin \baseof{C}
  53   \end{cases}
  54 }\]
  55
  56 \subsection{Tip Own Contents}
  57 Given Base Acyclic for $C$,
  58 $$
  59   \bigforall_{C \in \py} C \haspatch \p
  60 $$
  61 Ie, tip commits contain their own patch.
  62
  63 \proof{
  64 Apply Exclusive Tip Contents to some $D \in \py$:
  65 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
  66   D \isin C \equiv D \le C $.
  67 Thus $C \zhaspatch \p$.
  68 And we can set $F=C$ giving $F \in \py \land F \le C$, so $C \haspatch \p$.
  69 }
  70
  71 \subsection{Exact Ancestors}
  72 $$
  73   \bigforall_{ C \hasparents \set{R} }
  74   \left[
  75   D \le C \equiv
  76     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
  77     \lor D = C
  78   \right]
  79 $$
  80 \proof{ ~ Trivial.}
  81
  82 \subsection{Transitive Ancestors}
  83 $$
  84   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
  85   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
  86 $$
  87
  88 \proof{
  89 The implication from right to left is trivial because
  90 $ \pends() \subset \pancs() $.
  91 For the implication from left to right:
  92 by the definition of $\mathcal E$,
  93 for every such $A$, either $A \in \pends()$ which implies
  94 $A \le M$ by the LHS directly,
  95 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
  96 in which case we repeat for $A'$.  Since there are finitely many
  97 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
  98 by the LHS.  And $A \le A''$.
  99 }
 100
 101 \subsection{Calculation of Ends}
 102 $$
 103   \bigforall_{C \hasparents \set A}
 104     \pendsof{C}{\set P} =
 105       \begin{cases}
 106        C \in \set P : & \{ C \}
 107       \\
 108        C \not\in \set P : & \displaystyle
 109        \left\{ E \Big|
 110            \Bigl[ \Largeexists_{A \in \set A}
 111                        E \in \pendsof{A}{\set P} \Bigr] \land
 112            \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\set P}}
 113                        E \neq F \land E \le F \Bigr]
 114        \right\}
 115       \end{cases}
 116 $$
 117 \proof{
 118 Trivial for $C \in \set P$.  For $C \not\in \set P$,
 119 $\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
 120 So $\pendsof{C}{\set P} \subset \bigcup_{E \in \set E} \pendsof{E}{\set P}$.
 121 Consider some $E \in \pendsof{A}{\set P}$.  If $\exists_{B,F}$ as
 122 specified, then either $F$ is going to be in our result and
 123 disqualifies $E$, or there is some other $F'$ (or, eventually,
 124 an $F''$) which disqualifies $F$ and $E$.
 125 Otherwise, $E$ meets all the conditions for $\pends$.
 126 }
 127
 128 \subsection{Single Parent Unique Tips}
 129
 130 Unique Tips is satisfied for single-parent commits.  Formally,
 131 given a conformant commit $A$,
 132 $$
 133  \Big[
 134    C \hasparents \{ A \}
 135  \Big] \implies \left[
 136    \bigforall_{P \patchisin C} \pendsof{C}{\py} = \{ T \}
 137  \right]
 138 $$
 139 \proof{
 140   Trivial for $C \in \py$.
 141   For $C \not\in \py$, $\pancsof{C}{\py} = \pancsof{A}{\py}$,
 142   so Unique Tips of $A$ suffices.
 143 }
 144
 145 \subsection{Ingredients Prevent Replay}
 146 Given conformant commits $A \in \set A$,
 147 $$
 148   \left[
 149     {C \hasparents \set A} \land
 150    \\
 151     \bigforall_{D}
 152     \left(
 153        D \isin C \implies
 154        D = C \lor
 155        \Largeexists_{A \in \set A} D \isin A
 156     \right)
 157   \right] \implies \left[ \bigforall_{D}
 158     D \isin C \implies D \le C
 159   \right]
 160 $$
 161 \proof{
 162   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
 163   By the preconditions, there is some $A$ s.t. $A \in \set A$
 164   and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
 165   $A \le C$ so $D \le C$.
 166 }
 167
 168 \subsection{Simple Foreign Inclusion}
 169 Given a conformant commit $L$,
 170 $$
 171   \left[
 172     C \hasparents \{ L \}
 173    \land
 174     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
 175   \right]
 176  \implies
 177   \left[
 178    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
 179      D \isin C \equiv D \le C
 180   \right]
 181 $$
 182 \proof{
 183 Consider some $D$ s.t. $\patchof{D} = \bot$.
 184 If $D = C$, trivially true.  For $D \neq C$,
 185 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 186 And by Exact Ancestors $D \le L \equiv D \le C$.
 187 So $D \isin C \equiv D \le C$.
 188 }
 189
 190 \subsection{Totally Foreign Contents}
 191 Given conformant commits $A \in \set A$,
 192 $$
 193    \left[
 194     C \hasparents \set A \land
 195     \patchof{C} = \bot \land
 196       \bigforall_{A \in \set A} \patchof{A} = \bot
 197    \right]
 198   \implies
 199    \left[
 200   \bigforall_{D}
 201     D \le C
 202    \implies
 203     \patchof{D} = \bot
 204    \right]
 205 $$
 206 \proof{
 207 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
 208 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
 209 Contents of $A$, $\patchof{D} = \bot$.
 210 }
 211