[darcs-users] How conflictors work

David Roundy daveroundy at gmail.com
Sat May 17 11:18:21 UTC 2008


Hi Ian,

I've finally gotten around to reading this, and am writing down the
comments as I go.

First, as you know, I disagree with several of the statements in your "aside".

In particular, it is necessary to define a distinct inverse-catch
type.  Your approach of just inverting and throwing in a bunch of
context will fail.  Most likely you made this mistake through failing
to consider that the context in a "contexted patch" is not a sequence
of patches, but rather a sequence of catches, and inverses when added
to a context do not cancel one another out.

i.e. the contexted patch  pp^ : p is different from the contexted
patch :p.  It's highly inconvenient, but it's true.  If you made them
the same, you'd be unable to distinguish between distinct patches,
i.e. the rule that two patches which have the same contexted value in
the same context are the same patch would be violated.

Conjecture 4.5 conveniently is proven by the type system, so I think
you might be able to elevate it above the level of conjecture, at
least with regards to the actual darcs code.

In definition 4.7 (merge), I don't see why you restrict yourself to
the merging of conflicts where Esp and Esq are disjoint.  It's trivial
to construct an example where this isn't the case.  e.g. consider the
merge of three patches A, B and C that each modify the same line.
First you construct AB' and AC', and then you merge B' and C', both of
which have the same patch in their effect.

I think most of your conjectures 4.8 an4.9 are theorems if you define
the merge to be such that

p + q = <q', p'>  implies that pq' <-> qp'

so that then the properties of the commute define the properties of
the merge.  I suppose since your commute properties are expressed as
conjectures, these merge properties are still conjectures, but they
become redundant, once you define the relationship between merge and
commute (which is that commute is the asymmetrical inverse of merge).

However, your XXX comment in the merge definition should be all right:
 when the two effects are disjoint, they do not conflict.

Of course, this is conjecture 4.10, but it implies conjectures 4.8 and
4.9, which I would just cut, or mention only as sidenotes to 4.10.

Regarding your concern whether Z should be a bag, not a set, that's
why we treat identical patches as identical.  This is what makes Z a
set, since there can't be two distinct identical elements.  The whole
formalism is far more challenging if you allow distinct identical
patches.

I should also admit that when your paper got into dense mathematical
notation (e.g. section 2), I tuned out, since I don't know this
notation, and am insufficiently motivated to learn it at this
juncture.  I know that English is more verbose, but I prefer it.

David

On Fri, May 9, 2008 at 6:05 PM, Ian Lynagh <igloo at earth.li> wrote:
>
> Hi all,
>
> I've been trying to understand how conflictors work, prove that they do,
> and prove that they do quickly. So far I've mostly done the first of
> these  :-)
>
> Attached is what I've written. It probably has lots of little errors,
> plus at least couple of bigs ones (which are described in the last
> section), but I'm unlikely to spend more time on this for at least the
> next couple of weeks, so I thought I'd send it in case anyone else found
> it useful. It also isn't entirely formally specified, and the level of
> formality varies throughout.
>
> Currently it describes patches, lists the patch axioms we can assume,
> then goes on to describe catches (a catch is either a patch or a
> conflictor) and lists the properties we want to prove. I may have missed
> out some properties, axioms and explanations, of course!
>
> It actually differs from the darcs definition in a small number of
> details, but all those I know about are described in the file. It also
> ignores whatever it is that darcs2 does with duplicate patches.
>
> Attached is the PDF of the built document, along with all the files I
> need to build it.


More information about the darcs-users mailing list