[darcs-devel] [patch1701] refactorings in the Darcs.Patch subsystem

[Benjamin Franksen]

>>> We (have to) weaken the requirements for
>>> Commute (realtive to CommuteNoConflicts) precisely so that we can 
>>> state the merge commute law.
>>
>>> In this sense, the difference between CommuteNoConflicts
>>> and Commute precisely captures, in an abstract way, the
>>> difference in behavior between commute for prim patches
>>> and commute for generalized patches.
>>
>> Right. I think you've uncovered an important part of the "theory" of
>> darcs here (at least, I wasn't previously aware of it in these 
>> terms).
> 
> I think so, too. Uncovering this has cost me endless hours of headaches.
> None of publicly available sources talk about the breakdown of the
> square commute law anywhere. The camp paper, for instance, lists proving
> it for "Catches" as TODO.

I think David Roundy was aware of this at least partly. His side
condition for the square-commute law is another way to state one half of
it. To recap, he stated it as

  p:>q <--> q':>p' if and only if q'^:>p <--> p':>q^,
  but only if both commutes succeed.

He did not observe, though, at least not in any text available to me,
that the side condition can be dropped for prim patches, in other words,
that it is the presence of conflictors together with the merge-commute
law, that make the side condition necessary. I think my formulation
using commuteNoConflicts instead of the side condition makes this clearer.

Cheers
Ben

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.osuosl.org/pipermail/darcs-devel/attachments/20181120/a8d2986d/attachment.asc>