From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Wed, 8 Feb 2012 21:36:30 +0000 (+0000)
Subject: wip theory
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke.git;a=commitdiff_plain;h=5ae399ddff45b6edb446ee5d9b779fb91985e439

wip theory
---

diff --git a/THEORY b/THEORY
index e908c68..f5518b0 100644
--- a/THEORY
+++ b/THEORY
@@ -3,54 +3,85 @@ relations
 		C > D		C is a descendant of D
 	inclusion: commit includes change made in another
 		a partial order, consistent with ancestry but more partial
-		C ] D
-	C ] D => C > D
+		C has D <=> D isin C
+	C has D => C > D
+
+define convenience function
+	cont(C) := { Cx | Cx isin C }
 
 patches
-	patch P is two subset of commits, Ptip and Pbase
+	patch P is two sets Px of commits, Ptip and Pbase
 	each subset has a single ur-ancestor C0_Ptip resp C0_Pbase
-	these subsets mutually exclusive
+	all these subsets Ptip,Qbase,Rtip,Sbase mutually exclusive
 	P(C) is either Ptip, Pbase, or nil (recorded in commit)
 
 commits fall into three categories wrt P
- how(P,C) = included
+ inpatch(P,C) = included
 	P included in C
-		\forall D \elem Ptip,  C ] D <=> C > D
- how(P,C) = absent
+		\forall D \elem Ptip,  C has D <=> C > D
+ inpatch(P,C) = absent
 	P absent from C
-		\forall D \elem Ptip, !(C ] D)
- how(P,C) = removed
+		\forall D \elem Ptip, !(C has D)
+ inpatch(P,C) = removed
 	P removed from C
-		\exists E s.t.
-			\forall D \elem Ptip,
-				something
+		cont(C) \intersection Ptip = { }
+		but maybe \exists Cx \elem Ptip s.t. Cx < C
 
 the ends E(C,Px) of Px = Pbase or Ptip are
-	every maximal Ce < C in Px ie
-	every Ce for which
-		C > Ce   ^   !\exists C s.t. C > Ce
+	every maximal Ce < C in Px
+	ie every Ce for which
+		C > Ce   and   !\exists C s.t. C > Ce
+
+existence of corresponding base B for every tip commit C
+	\forall C s.t. P(C) = Ptip
+		\exists B s.t. E(C,Pbase) = { B }
+ resulting function B(C)
+
+contents of tip commits
+	\forall C s.t. P(c) = Ptip
+		cont(C) = cont(B(C)) \union { Cp s.t. P(Cp) = Ptip and Cp < C }
 
-cleanness of patch
-	if P(C) = Ptip
-	   B \elem E(C,Pbase)
-	then
-	   C ] Cx  ^  B !] Cx  =>  P
+non-circularity
+	\forall B s.t. P(c) = Pbase
+		cont(B) \notintersect Ptip
 
 normal commits
  make C from D
  result
 	C < { D }
 	P(C) = P(D)
-	Cx [ C  <=>  Cx = D  v  Cx [ D
-	how(P,C) = how(P,D)
+	Cx isin C  <=>  Cx = D  v  Cx isin D
+	inpatch(P,C) = inpatch(P,D)
 
-anticommit
- make C from D, P, A-, A+ 
+anticommit for removing a patch P from D to make C
+ make C from D, A-
  where
-	A+ < A- < D
+	P(C) = Qbase
+	P(A-) = Ptip
+	inpatch(P,C) = included
 	E(D,Ptip) = { A- }
+ then let
+	A+ = B(A-)
+ hence
+	A+ < A- < D
 	E(D,Pbase) = { A+ }
  result
-	C < { D }
+	C >1 { D }
 	P(C) = P(D)
-	
+	inpatch(P,C) = removed
+
+single patch dependency application
+ make C from D, A+
+ where
+	P(C) = Qbase
+	P(A+) = Ptip
+	inpatch(P,C) != included
+ then let
+	A- = B(A+)
+ hence
+	A- < A+
+ result
+	C >1 { D, A+ } => C > D, C > A+ > A-
+	P(C) = P(D)
+	inpatch(P,C) = included
+