I've been trying to put together a proof, and ran into a strange
example: what if AB and B' are both repositories, but A and B don't
commute? I.e. A can only be applied if B hasn't been applied yet, but B
doesn't depend on A.
My questions: Is this situation disallowed by some existing patch
theory formalization? Is there a good reason to rule it out? Is it
actually possible in Darcs? (I doubt the last one.)
As far as I can tell, the example is consistent with the patch theory
axioms in [0] and [1]: we can simply say that in our patch theory,
nothing ever commutes, and then the axioms don't have much to say.
The Camp theory pdf [2] makes a claim that seems to rule out the
example: in section 8.1, "Merge preparation", it's asserted that as a
first step toward merging two repos, we can move the common patches to
the beginning. In this case, that would imply B can be moved to the
beginning of the repo AB. However, I'm not sure where that's proved,
and I also can't see why the above situation is inconsistent with the
axioms in that write-up. (Admittedly, I haven't read it completely ---
if someone can point me to the right parts, I'd appreciate it.)
In practice, I suspect it can't happen in Darcs, but I could imagine
maybe someone would want a patch theory where it's possible. For
example, maybe A reverses the order of lines in a file, and B deletes
that file.
I'm interested in this because I think the following property would be
useful for reasoning about repositories, but the example contradict it.
Property:
(Summary: any sequence of patch names can be realized as a sequence of
patches unless there's a specific conflict or violated dependency
preventing it.)
Let N be the set of (positive) patch names and C(N) the set of finite
subsets of N.
There exist:
- a function "minimal_context" : N -> C(N);
- a relation "conflict" on N x N; and
- a universal starting context "empty_repo"
such that the following properties hold. (Note that the above three
objects are independent of any particular repository, so I'm asserting
for example that minimal contexts are universal.)
1. conflict is symmetric (conflict(a,b) implies conflict(b, a)).
2. Consistency of minimal_context and conflict:
For any names n1 and n2, at most one of the following is true:
- n1 is in minimal_context(n2)
- n2 is in minimal_context(n1)
- conflict(n1, n2)
3. Let n_1, n_2, ..., n_k be a sequence of distinct patch names
satisfying the following:
- No patches in the sequence conflict: for all 1 <= i < j <= k,
conflict(n_i, n_j) is false.
- Dependencies are satisfied: for all 1 <= i <= k, every element of
minimal_context(n_i) appears somewhere before n_i in the sequence.
Then there exists a (unique) patch sequence P_1 ... P_k with names
n_1 ... n_k which can be applied starting at empty_repo.
[0] Ganesh Sittampalam et al. "Some properties of darcs patch theory".
November 7, 2005. Downloaded 2020-11-21 from
https://urchin.earth.li/darcs/ganesh/darcs-patch-theory/theory/formal.pdf
[1] Judah Jacobson, "A Formalization of Darcs patch theory using
inverse semigroups". Downloaded 2020-06-21 from
ftp://ftp.math.ucla.edu/pub/camreport/cam09-83.pdf
[2] Camp theory.pdf, downloaded 2020-06-21 from
https://archives.haskell.org/projects.haskell.org/camp/files/theory.pdf
--
James
_______________________________________________
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
