Re: [darcs-users] How to extend a patch theory to fully commute
Am 19.08.20 um 11:44 schrieb Ben Franksen: > The fact that your patches have no "content" is of of course a result of > starting out with "enriched" contexts. As you note in 2.2 > Interpretation, your contexts can *not* in general be understood simply > as "working tree states": the mapping from contexts to states is not > injective. It is not yet clear to me if that will have consequences when > it comes to implementing your theory. Let me elaborate this point a bit. Your theory assume the existence of contexts as a "set". That doesn't give us any hint as to how these contexts should be represented in a concrete implementation. If we start out with some notion of prim patch (such as the one in Darcs), then these exist as concrete representations of state changes as data. But we know that states do not correspond 1:1 to contexts. The simplest example involves duplicate prim patches p, q, such that name(p)/=name(q), but repr(p)==repr(q). Assuming a starting context X for both p and q, the ending context is different, even though the end state is the same. More interesting examples involve things like (remove f; add g) versus (move f g). The question now is: how can we arrive at a suitable definition (i.e. representation) of context, given such a concrete definition of prim patches and states? The answer, in Darcs at least, is to not define contexts. Contexts aren't represented at runtime at all. Instead, in our code contexts exist only formally at the type level. Your definition of context address may require that we have a way to reify contexts as data. A natural way of arriving at a suitable definition is to go backwards from patches: identify a context with the set of all patch sequences that start at the empty state and that differ only by commutation. At this point I am always tempted to say "and elimination of inverses"; indeed your definition of a patch universe implies that a sequence [a;b;b^] really has the same start and end context as the plain [a]. But with respect to commutation this doesn't seem right: [a;c] may commute to some [c';a'], but [a;b;b^;c] may not, because e.g. [a;b] may not commute. Every time I think about this I am getting head-aches. I cannot reconcile these two points of view. Anyway, assuming we have sorted this out somehow, I am still having doubts about reifying contexts, because the definition as an equivalence class of sequences does not easily map to an efficient representation. Cheers Ben ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] How to extend a patch theory to fully commute
Am 19.08.20 um 03:26 schrieb James Cook: >> I changed the definition of Context >> Address to work better with my new "patch universe" definition, but I >> think it amounts to the same thing. > > Thinking about it more, I'm not sure my new definition of Context > Address is a good one, since I've been finding it hard to associate a > primitive context with every minimal context address in the same way I > did in the hms_patchfinder writeup. > > It might be better to stick closer to my original definition of > context address. The proof should still be about as easy as the one in > the linked pdf: if a context address points to two different contexts, > you can conclude the contexts are equal because a name-balanced path > connects. them. I agree; your new definition is too general: you allow arbitrary signed name multisets; whereas your original definition started out with a valid sequence. Cheers Ben ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] How to extend a patch theory to fully commute
Am 18.08.20 um 22:42 schrieb James Cook: > Okay, I wrote something up: https://www.falsifian.org/a/xxOw/misc.pdf I like it. Especially the part where you define commutation in terms of the balance-respecting property. This is very elegant. It confirms what I have long since suspected, namely that the whole theory becomes simpler and more regular if we concentrate on patch /sequences/ instead of individual patches. The fact that your patches have no "content" is of of course a result of starting out with "enriched" contexts. As you note in 2.2 Interpretation, your contexts can *not* in general be understood simply as "working tree states": the mapping from contexts to states is not injective. It is not yet clear to me if that will have consequences when it comes to implementing your theory. One a minor note, your patch universe definition is not suitable for extended patches as defined in Darcs: For these, the square commute law (which you call rotation, perhaps a better name) does not hold. Though to be fair, a while ago we have stopped treating them as invertible in the first place, so nowadays we couldn't even /state/ that property for them. (This remark is largely irrelevant for your theory.) I'll comment on the new context address definition in another message. Cheers Ben ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
