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

List:       darcs-conflicts
Subject:    Re: [darcs-conflicts] Patch calculus: expressing 'same effect'
From:       Marnix Klooster <marnix.klooster () gmail ! com>
Date:       2005-05-10 5:03:15
Message-ID: 42804093.3060105 () gmail ! com
[Download RAW message or body]

Ganesh Sittampalam wrote:

>Hi Marnix (and others),
>
>On Mon, 9 May 2005, Marnix Klooster wrote:
>
>  
>
>>Today I was thinking a bit about how to express formally the
>>relationship between the conflictor [A,B] and its intended effect
>>inv(A).  And then I discovered that, for A || B, we have already enough
>>notation to express "A has the same effect as B":
>>
>>    inv(A) || inv(B)
>>
>>This says that the inverses of A and B have the same (initial) context,
>>i.e., that A and B have the same (resulting) context.
>>    
>>
>
>I don't think this is right.
>
I think we agree in essence, but use different terminology.  See below.

>We have to make a distinction between the
>patches listed in the context and the state of the tree;
>
Agreed.  The first one I call the 'meaning' (of all patches that
produced the tree), and the state of the tree I call 'context'. 
(Confusing, perhaps...)

>[A,B] leaves A in
>the context and adds B, but reverts A from the state of the tree. So we
>end up with a context that claims to have both A and B in some form, but
>an associated tree that has the effects of neither.
>  
>
Yes.  In my terminology: the tree (=context) of patch A (i.e., the tree
that it applies to) is the same as the tree that results from A[A,B]. 
The meaning, however, of A[A,B] is (informally) "both A and B".

>A || B and inv(A) || inv(B) means that A and B start from the same context
>and end at the same context, which means they must be the same patch, i.e.
>A=B, I think.
>  
>
Using your definition of A=B ("identity(A) = identity(B) and
context(A) = context(B)"), we can only conclude this if A and B have the
same identity.  In the specific case I was discussing: we cannot
conclude that A[A,B] = null@A, because the LHS has identity {A,B}, and
the other {} ("do nothing").

Another related thing: David said that in the expression [A,B]C all
patches are parallel: A||B||C.  This can only follow from inv([A,B]) ||
A, or a similar kind of axiom.  Do you agree?

Groetjes,
 <><
Marnix

_______________________________________________
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]