chiark / gitweb /
add FIXME because \py seems to cause barf in \subsubsection
[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   E \neq A \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 \[ \eqn{Calculation Of Ends:}{
223   \bigforall_{C \hasparents \set A}
224     \pendsof{C}{\set P} =
225        \Bigl\{ E \Big|
226            \Bigl[ \Largeexists_{A \in \set A} 
227                        E \in \pendsof{A}{\set P} \Bigr] \land
228            \Bigl[ \Largenexists_{B \in \set A} 
229                        E \neq B \land E \le B \Bigr]
230        \Bigr\}
231 }\]
232 XXX proof TBD.
233
234 \section{Commit annotation}
235
236 We annotate each Topbloke commit $C$ with:
237 \gathbegin
238  \patchof{C}
239 \gathnext
240  \baseof{C}, \text{ if } C \in \py
241 \gathnext
242  \bigforall_{\pa{Q}} 
243    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
244 \gathnext
245  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
246 \end{gather}
247
248 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
249 make it wrong to make plain commits with git because the recorded $\pends$
250 would have to be updated.  The annotation is not needed because
251 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
252
253 \section{Simple commit}
254
255 A simple single-parent forward commit $C$ as made by git-commit.
256 \begin{gather}
257 \tag*{} C \hasparents \{ A \} \\
258 \tag*{} \patchof{C} = \patchof{A} \\
259 \tag*{} D \isin C \equiv D \isin A \lor D = C
260 \end{gather}
261
262 \subsection{No Replay}
263 Trivial.
264
265 \subsection{Unique Base}
266 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
267
268 \subsection{Tip Contents}
269 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
270 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
271 Substitute into the contents of $C$:
272 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
273     \lor D = C \]
274 Since $D = C \implies D \in \py$, 
275 and substituting in $\baseof{C}$, this gives:
276 \[ D \isin C \equiv D \isin \baseof{C} \lor
277     (D \in \py \land D \le A) \lor
278     (D = C \land D \in \py) \]
279 \[ \equiv D \isin \baseof{C} \lor
280    [ D \in \py \land ( D \le A \lor D = C ) ] \]
281 So by Exact Ancestors:
282 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
283 ) \]
284 $\qed$
285
286 \subsection{Base Acyclic}
287
288 Need to consider only $A, C \in \pn$.  
289
290 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
291
292 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
293 $A$, $D \isin C \implies D \not\in \py$. $\qed$
294
295 \subsection{Coherence and patch inclusion}
296
297 Need to consider $D \in \py$
298
299 \subsubsection{For $A \haspatch P, D = C$:}
300
301 Ancestors of $C$:
302 $ D \le C $.
303
304 Contents of $C$:
305 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
306
307 \subsubsection{For $A \haspatch P, D \neq C$:}
308 Ancestors: $ D \le C \equiv D \le A $.
309
310 Contents: $ D \isin C \equiv D \isin A \lor f $
311 so $ D \isin C \equiv D \isin A $.
312
313 So:
314 \[ A \haspatch P \implies C \haspatch P \]
315
316 \subsubsection{For $A \nothaspatch P$:}
317
318 Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
319 Thus $D \neq C$.
320
321 Now by contents of $A$, $D \notin A$, so $D \notin C$.
322
323 So:
324 \[ A \nothaspatch P \implies C \nothaspatch P \]
325 $\qed$
326
327 \subsection{Foreign inclusion:}
328
329 If $D = C$, trivial.  For $D \neq C$:
330 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
331
332 \section{Merge}
333
334 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
335 \gathbegin
336  C \hasparents \{ L, R \}
337 \gathnext
338  \patchof{C} = \patchof{L}
339 \gathnext
340  D \isin C \equiv
341   \begin{cases}
342     (D \isin L \land D \isin R) \lor D = C : & \true \\
343     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
344     \text{otherwise} : & D \not\isin M
345   \end{cases}
346 \end{gather}
347
348 \subsection{Conditions}
349
350 \[ \eqn{ Tip Merge }{
351  L \in \py \implies
352    \begin{cases}
353       R \in \py : & \baseof{R} \ge \baseof{L}
354               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
355       R \in \pn : & R \ge \baseof{L}
356               \land M = \baseof{L} \\
357       \text{otherwise} : & \false
358    \end{cases}
359 }\]
360
361 \subsection{No Replay}
362
363 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
364
365 \subsubsection{For $D \isin L \land D \isin R$:}
366 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
367
368 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
369 $D \not\isin C$.  OK.
370
371 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
372 $D \not\isin C$.  OK.
373
374 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
375  \land D \not\isin M$:}
376 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
377 R$ so $D \le C$.  OK.
378
379 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
380  \land D \isin M$:}
381 $D \not\isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
382 R$ so $D \le C$.  OK.
383
384 $\qed$
385
386 \subsection{Unique Base}
387
388 Need to consider only $C \in \py$, ie $L \in \py$,
389 and calculate $\pendsof{C}{\pn}$.  So we will consider some
390 putative ancestor $A \in \pn$ and see whether $A \le C$.
391
392 $A \le C \equiv A \le L \lor A \le R \lor A = C$.
393 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
394 Thus $A \le L \lor A \le R$.
395
396 By Unique Base of L and Transitive Ancestors,
397 $A \le L \equiv A \le \baseof{L}$.
398
399 \subsubsection{For $R \in FIXME py$:}
400
401 By Unique Base of $R$ and Transitive Ancestors,
402 $A \le R \equiv A \le \baseof{R}$.
403
404 But by Tip Merge condition on $\baseof{R}$,
405 $A \le \baseof{L} \implies A \le \baseof{R}$, so
406 $A \le \baseof{R} \lor A \le \baseof{R} \equiv A \le \baseof{R}$.
407 Thus $A \le C \equiv A \le \baseof{R}$.  Ie, $\baseof{C} =
408 \baseof{R}$.
409
410 UP TO HERE
411
412 By Tip Merge, $A \le $
413
414 Let $S =
415    \begin{cases} 
416      R \in \py : & \baseof{R} \\
417      R \in \pn : & R
418    \end{cases}$.  
419 Then by Tip Merge $S \ge \baseof{L}$, and $R \ge S$ so $C \ge S$.
420    
421 Consider some $A \in \pn$.  If $A \le S$ then $A \le C$.
422 If $A \not\le S$ then 
423
424 Let $A \in \pends{C}{\pn}$.  
425 Then by Calculation Of Ends $A \in \pendsof{L,\pn} \lor A \in
426 \pendsof{R,\pn}$.
427
428
429
430 %$\pends{C,
431
432 %%\subsubsection{For $R \in \py$:}
433
434 \end{document}