chiark / gitweb /
Largeexists
[topbloke-formulae.git] / article.tex
1 \documentclass[a4paper,leqno]{strayman}
2 \let\numberwithin=\notdef
3 \usepackage{amsmath}
4 \usepackage{mathabx}
5 \usepackage{txfonts}
6 \usepackage{amsfonts}
7 \usepackage{mdwlist}
8 %\usepackage{accents}
9
10 \renewcommand{\ge}{\geqslant}
11 \renewcommand{\le}{\leqslant}
12
13 \newcommand{\has}{\sqsupseteq}
14 \newcommand{\isin}{\sqsubseteq}
15
16 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
17 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
18 \newcommand{\haspatch}{\sqSupset}
19 \newcommand{\patchisin}{\sqSubset}
20
21 \newcommand{\set}[1]{\mathbb #1}
22 \newcommand{\pa}[1]{\varmathbb #1}
23 \newcommand{\pay}[1]{\pa{#1}^+}
24 \newcommand{\pan}[1]{\pa{#1}^-}
25
26 \newcommand{\p}{\pa{P}}
27 \newcommand{\py}{\pay{P}}
28 \newcommand{\pn}{\pan{P}}
29
30 %\newcommand{\hasparents}{\underaccent{1}{>}}
31 %\newcommand{\hasparents}{{%
32 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
33 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
34 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
35
36 \renewcommand{\implies}{\Rightarrow}
37 \renewcommand{\equiv}{\Leftrightarrow}
38 \renewcommand{\land}{\wedge}
39 \renewcommand{\lor}{\vee}
40
41 \newcommand{\pancs}{{\mathcal A}}
42 \newcommand{\pends}{{\mathcal E}}
43
44 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
45 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
46
47 \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
48 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
49
50 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
51 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
52
53 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
54 \newcommand{\bigforall}{%
55   \mathop{\mathchoice%
56     {\hbox{\huge$\forall$}}%
57     {\hbox{\Large$\forall$}}%
58     {\hbox{\normalsize$\forall$}}%
59     {\hbox{\scriptsize$\forall$}}}%
60 }
61
62 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
63 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
64
65 \newcommand{\qed}{\square}
66 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
67
68 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
69 \newcommand{\gathnext}{\\ \tag*{}}
70
71 \newcommand{\true}{t}
72 \newcommand{\false}{f}
73
74 \begin{document}
75
76 \section{Notation}
77
78 \begin{basedescript}{
79 \desclabelwidth{5em}
80 \desclabelstyle{\nextlinelabel}
81 }
82 \item[ $ C \hasparents \set X $ ]
83 The parents of commit $C$ are exactly the set
84 $\set X$.
85
86 \item[ $ C \ge D $ ]
87 $C$ is a descendant of $D$ in the git commit
88 graph.  This is a partial order, namely the transitive closure of 
89 $ D \in \set X $ where $ C \hasparents \set X $.
90
91 \item[ $ C \has D $ ]
92 Informally, the tree at commit $C$ contains the change
93 made in commit $D$.  Does not take account of deliberate reversions by
94 the user or reversion, rebasing or rewinding in
95 non-Topbloke-controlled branches.  For merges and Topbloke-generated
96 anticommits or re-commits, the ``change made'' is only to be thought
97 of as any conflict resolution.  This is not a partial order because it
98 is not transitive.
99
100 \item[ $ \p, \py, \pn $ ]
101 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
102 are respectively the base and tip git branches.  $\p$ may be used
103 where the context requires a set, in which case the statement
104 is to be taken as applying to both $\py$ and $\pn$.
105 All these sets are distinct.  Hence:
106
107 \item[ $ \patchof{ C } $ ]
108 Either $\p$ s.t. $ C \in \p $, or $\bot$.  
109 A function from commits to patches' sets $\p$.
110
111 \item[ $ \pancsof{C}{\set P} $ ]
112 $ \{ A \; | \; A \le C \land A \in \set P \} $ 
113 i.e. all the ancestors of $C$
114 which are in $\set P$.
115
116 \item[ $ \pendsof{C}{\set P} $ ]
117 $ \{ E \; | \; E \in \pancsof{C}{\set P}
118   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
119   A \neq E \land E \le A \} $ 
120 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
121
122 \item[ $ \baseof{C} $ ]
123 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
124 A partial function from commits to commits.
125 See Unique Base, below.
126
127 \item[ $ C \haspatch \p $ ]
128 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
129 ~ Informally, $C$ has the contents of $\p$.
130
131 \item[ $ C \nothaspatch \p $ ]
132 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
133 ~ Informally, $C$ has none of the contents of $\p$.  
134
135 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
136 patch is applied to a non-Topbloke branch and then bubbles back to
137 the Topbloke patch itself, we hope that git's merge algorithm will
138 DTRT or that the user will no longer care about the Topbloke patch.
139
140 \end{basedescript}
141 \newpage
142 \section{Invariants}
143
144 We maintain these each time we construct a new commit. \\
145 \[ \eqn{No Replay:}{
146   C \has D \implies C \ge D
147 }\]
148 \[\eqn{Unique Base:}{
149  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
150 }\]
151 \[\eqn{Tip Contents:}{
152   \bigforall_{C \in \py} D \isin C \equiv
153     { D \isin \baseof{C} \lor \atop
154       (D \in \py \land D \le C) }
155 }\]
156 \[\eqn{Base Acyclic:}{
157   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
158 }\]
159 \[\eqn{Coherence:}{
160   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
161 }\]
162 \[\eqn{Foreign Inclusion:}{
163   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
164 }\]
165
166 \section{Some lemmas}
167
168 \[ \eqn{Exclusive Tip Contents:}{
169   \bigforall_{C \in \py} 
170     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
171       \Bigr]
172 }\]
173 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
174
175 \proof{
176 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
177 So by Base Acyclic $D \isin B \implies D \notin \py$.
178 }
179 \[ \corrolary{
180   \bigforall_{C \in \py} D \isin C \equiv
181   \begin{cases}
182     D \in \py : & D \le C \\
183     D \not\in \py : & D \isin \baseof{C}
184   \end{cases}
185 }\]
186
187 \[ \eqn{Tip Self Inpatch:}{
188   \bigforall_{C \in \py} C \haspatch \p
189 }\]
190 Ie, tip commits contain their own patch.
191
192 \proof{
193 Apply Exclusive Tip Contents to some $D \in \py$:
194 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
195   D \isin C \equiv D \le C $
196 }
197
198 \[ \eqn{Exact Ancestors:}{
199   \bigforall_{ C \hasparents \set{R} }
200   D \le C \equiv
201     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
202     \lor D = C
203 }\]
204
205 \[ \eqn{Transitive Ancestors:}{
206   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
207   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
208 }\]
209
210 \proof{
211 The implication from right to left is trivial because
212 $ \pends() \subset \pancs() $.
213 For the implication from left to right: 
214 by the definition of $\mathcal E$,
215 for every such $A$, either $A \in \pends()$ which implies
216 $A \le M$ by the LHS directly,
217 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
218 in which case we repeat for $A'$.  Since there are finitely many
219 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
220 by the LHS.  And $A \le A''$.
221 }
222
223 \section{Commit annotation}
224
225 We annotate each Topbloke commit $C$ with:
226 \gathbegin
227  \patchof{C}
228 \gathnext
229  \baseof{C}, \text{ if } C \in \py
230 \gathnext
231  \bigforall_{\pa{Q}} 
232    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
233 \gathnext
234  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
235 \end{gather}
236
237 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
238 make it wrong to make plain commits with git because the recorded $\pends$
239 would have to be updated.  The annotation is not needed because
240 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
241
242 \section{Simple commit}
243
244 A simple single-parent forward commit $C$ as made by git-commit.
245 \begin{gather}
246 \tag*{} C \hasparents \{ A \} \\
247 \tag*{} \patchof{C} = \patchof{A} \\
248 \tag*{} D \isin C \equiv D \isin A \lor D = C
249 \end{gather}
250
251 \subsection{No Replay}
252 Trivial.
253
254 \subsection{Unique Base}
255 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
256
257 \subsection{Tip Contents}
258 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
259 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
260 Substitute into the contents of $C$:
261 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
262     \lor D = C \]
263 Since $D = C \implies D \in \py$, 
264 and substituting in $\baseof{C}$, this gives:
265 \[ D \isin C \equiv D \isin \baseof{C} \lor
266     (D \in \py \land D \le A) \lor
267     (D = C \land D \in \py) \]
268 \[ \equiv D \isin \baseof{C} \lor
269    [ D \in \py \land ( D \le A \lor D = C ) ] \]
270 So by Exact Ancestors:
271 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
272 ) \]
273 $\qed$
274
275 \subsection{Base Acyclic}
276
277 Need to consider only $A, C \in \pn$.  
278
279 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
280
281 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
282 $A$, $D \isin C \implies D \not\in \py$. $\qed$
283
284 \subsection{Coherence and patch inclusion}
285
286 Need to consider $D \in \py$
287
288 \subsubsection{For $A \haspatch P, D = C$:}
289
290 Ancestors of $C$:
291 $ D \le C $.
292
293 Contents of $C$:
294 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
295
296 \subsubsection{For $A \haspatch P, D \neq C$:}
297 Ancestors: $ D \le C \equiv D \le A $.
298
299 Contents: $ D \isin C \equiv D \isin A \lor f $
300 so $ D \isin C \equiv D \isin A $.
301
302 So:
303 \[ A \haspatch P \implies C \haspatch P \]
304
305 \subsubsection{For $A \nothaspatch P$:}
306
307 Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
308 Thus $D \neq C$.
309
310 Now by contents of $A$, $D \notin A$, so $D \notin C$.
311
312 So:
313 \[ A \nothaspatch P \implies C \nothaspatch P \]
314 $\qed$
315
316 \subsection{Foreign inclusion:}
317
318 If $D = C$, trivial.  For $D \neq C$:
319 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
320
321 \section{Merge}
322
323 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
324 \gathbegin
325  C \hasparents \{ L, R \}
326 \gathnext
327  \patchof{C} = \patchof{L}
328 \gathnext
329  D \isin C \equiv
330   \begin{cases}
331     (D \isin L \land D \isin R) \lor D = C : & \true \\
332     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
333     \text{otherwise} : & D \not\isin M
334   \end{cases}
335 \end{gather}
336
337 \subsection{Conditions}
338
339 \[ \eqn{ Tip Merge }{
340  L \in \py \implies
341    \begin{cases}
342       R \in \py : & \baseof{R} \ge \baseof{L}
343               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
344       R \in \pn : & R \ge \baseof{L}
345               \land M = \baseof{L} \\
346       \text{otherwise} : & \false
347    \end{cases}
348 }\]
349
350 \subsection{No Replay}
351
352 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
353
354 \subsubsection{For $D \isin L \land D \isin R$:}
355 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
356
357 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
358 $D \not\isin C$.  OK.
359
360 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
361 $D \not\isin C$.  OK.
362
363 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
364  \land D \not\isin M$:}
365 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
366 R$ so $D \le C$.  OK.
367
368 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
369  \land D \isin M$:}
370 $D \not\isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
371 R$ so $D \le C$.  OK.
372
373 $\qed$
374
375 \end{document}