[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)

Heinrich Apfelmus apfelmus at quantentunnel.de
Fri Oct 30 15:35:36 UTC 2009


Max Battcher wrote:
> I'm probably similarly confused as Eric, if not more so... Excuse my
> ignorance here, but I am interested in the practical repercussions of
> these discussions even if I can't bring much to the table on the
> theoretical side.
> 
>> Heinrich Apfelmus wrote:
>>> In any case, I once again would like to stress that it is my belief that
>>> commutation is already too complicated to be a suitable foundation for
>>> understanding the semantics of merges.
>>>
>>> In other words, thinking about the intricacies of commutation is a waste
>>> of our precious brain cycles. :) They are better spent on a simpler
>>> formalization where each line has its own GUID.
> 
> A GUID for each line? Is this primarily to make the proofs of darcs
> theory better sync with OT (and/or other similar theories), or is this
> also a practical concern?

Theory, mostly.

> That is, is the assertion here that darcs itself should use a GUID for
> every single line? Wouldn't that be woefully inefficient?

Yes and yes. That's why a more efficient representation or maybe
backporting GUIDs to commutations might be probably necessary.

> From a purely layman's standpoint it seems to me that as intricate as
> darcs commutation can get it appears to get the job done and that GUID's
> are rarely the answer to anything (other than how do we embroil this
> existing system with lots of rarely used cryptic strings).

Well, it gets the job done until you're trying to do heavy merges ...

I'm no fan of cryptic numbers, I just mean some scheme with some unique
identifiers. The advantage of IDs is the following: in the current
system, you have to change the patch representation when performing a
commutation

     Insert "foo" before line 1

     Change line 2 from "bar" to "baz"

  <->

     Change line 1 from "bar" to "baz"

     Insert "foo" before line 1

But with IDs, the representation can stay the same

     Create new line called B
     Set text of B to "foo"
     Link B as previous line of A

     Change text of line A from "bar" to "baz"

  <->

     Change text of line A from "bar" to "baz"

     Create new line called B
     Set text of B to "foo"
     Link B as previous line of A

which makes it much easier to reason about.


Regards,
apfelmus

--
http://apfelmus.nfshost.com



More information about the darcs-users mailing list