[prev in list] [next in list] [prev in thread] [next in thread] 

List:       darcs-conflicts
Subject:    Re: [darcs-conflicts] What is the effect of [P;
From:       Marnix Klooster <marnix.klooster () gmail ! com>
Date:       2005-09-07 7:48:38
Message-ID: df1596cf05090700483925dcab () mail ! gmail ! com
[Download RAW message or body]

Hi David and others,

Just a quick response after a long time.  I hadn't replied to this
e-mail, because David seemed to be right with his examples in
opposition of axioms (2) and (5).

However, last night I very briefly looked at a print-out of this
e-mail, and noticed something worrying: (5) isn't an axiom, it's a
theorem.  Which means that either my formalization is wrong, or
David's counterexample is wrong.

Let me quote the relevant parts of our mails:

On 5/11/05, David Roundy <droundy@abridgegame.org> wrote:
> On Tue, May 10, 2005 at 09:25:56PM +0200, Marnix Klooster wrote:

> > TERMINOLOGY AND NOTATIONS
> >
> > First, let me try to define my terminology.  In this post I'll use
> > "tree" instead of "context" for clarity.  Every patch is fully defined
> > by its "input tree" and its "meaning".  (Think of the meaning as the
> > darcs patch identity, or identities (perhaps also 'negative') in case of
> > a composite patch.)  Together, the input tree and the meaning fully
> > determine the "output tree".
> >
> > I'll write A || B for "A and B have the same input tree".  (This is what
> > I actually meant all along, but never made explicit.)  Since all patches
> > are invertible, inv(A) || inv(B) means "A and B have the same output
> > tree".  I'll write A ~~ B for "A and B have the same meaning".  A ~~ B
> > implies inv(A) ~~ inv(B).
[snip]
> > As before, I'll write <A,B> (only allowed if A||B) for "(the patch with
> > the meaning of) B, but applicable to the output tree of A".

> > AXIOMS AND THEOREMS
> >
> > The axioms that I will use below, and that I mentioned in earlier
> > e-mails (numbered for ease of reference):
> >
> > (1) <A,B> || inv(A)           "output tree of A is equal to input tree
> > of <A,B>"
[snip]
> > There is one new axiom that I need, which is key in what follows:
> >
> > (5) A || B  /\  inv(A) || inv(B)   =>   <A,C> = <B,C>
> >
> > Informally, if A and B transform the same input tree to the same output
> > tree (but perhaps have a different "meaning"), then it doesn't matter
> > whether we add A or B to the input tree of C.  That seems sensible,
> > doesn't it?

Actually, (5) isn't an axiom, as it directly follows from the stronger

(5')  inv(A) || inv(B)  ==  <A,C> = <B,C>

The proof is really trivial:

   <A,C> = <B,C>
==   "definition of patch equality"
   <A,C> || <B,C>  /\  <A,C> ~~ <B,C>
==   "LHS: (1), twice; RHS: <P,Q> ~~ Q, twice"
   inv(A) || inv(B)  /\  C ~~ C
==   "RHS: ~~ is reflexive"
   inv(A) || inv(B)

To derive this, as far as I can see we only need:

 - definition of patch equality ("same meaning applied to same tree");

 - (1) ("output tree of A is equal to input tree of <A,B>");

 - <P,Q> ~~ Q ("moving a patch does not change meaning")

However, David has a counterexample:

> No, this is wrong because two patches with the "same effect" can in fact
> have different commutation behaviors.  Take
> 
> A:
> 
> hunk 1 (line 1, that is)
> -hi world
> +hello world
> 
> B:
> 
> replace hi hello
> 
> Acting on a file in which there is only one instance of "hello", these two
> patches have the same effect.
> 
> But now let's try to merge them with a third patch
> 
> C:
> 
> hunk 5
> -I like to greet people.
> +I like to say hi to people.
> 
> When I do a merge, there's no conflict in either case, but
> 
> <A,C> = C (they're patches to different lines, and commute trivially)
> 
> <B,C>:
> 
> hunk 5
> -I like to greet people.
> +I like to say hello to people.

So this counterexample must violate of the assumptions I make in my
formalization above.  I don't have time to dive into this further
right now, but thought you'd like to know.  As I said, I suspect the
sematics of replace patches.  But I haven't yet put my finger on it,
and I've been known to be wrong before. :-)

Groetjes,
 <><
Marnix
--
Marnix Klooster
marnix.klooster@gmail.com

_______________________________________________
darcs-conflicts mailing list
darcs-conflicts@darcs.net
http://www.abridgegame.org/cgi-bin/mailman/listinfo/darcs-conflicts

[prev in list] [next in list] [prev in thread] [next in thread]