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

List:       darcs-conflicts
Subject:    Re: Patch calculus (was: Re: [darcs-conflicts] Conflictor notation
From:       Marnix Klooster <marnix.klooster () gmail ! com>
Date:       2005-04-30 14:17:56
Message-ID: 42739394.5040003 () gmail ! com
[Download RAW message or body]

David Roundy wrote:

>On Sat, Apr 30, 2005 at 11:57:40AM +0200, Marnix Klooster wrote:
>  
>
[snipped part where I take 'context addition' as primitive, instead of
commutation]

>Yeah, and that's a point where we tend to differ.  It's a question of how
>many constraints you need to write (or axioms), and how easily they are
>written in each representation.  My recollection is that there are about
>four properties that a commute must satisfy (plus their combinations, of
>course, which follow mathematically, but in terms of code verification
>should be tested separately in order to leverage our test cases), and that
>these are easiest to check on the commute function than the 'context
>addition' function.  Intuitively, 'context addition' just seems like half a
>function to me, but maybe that's because I've been thinking commutation for
>so long.
>  
>
Could be.  We'll see how things work out.  And it is also possible that
the simplest theory uses one, and the implementation that's most easy to
test uses the other.  For now I'll continue with having context addition
as primitive.

>>Yes, you're right, and although I thought about that while I wrote it, I
>>didn't take the time to elaborate.  To make this formally more correct,
>>we could e.g. write id@A for 'the patch with the same context as A, and
>>the change-nothing meaning".  However, for A+B or <A,B> to be meaningful
>>we have to know already that A||B.  So, for example, from the expression
>>A+id we can infer that id really means id@A.  As far as I can see we can
>>*always* infer the context of an 'id' patch in this way, making the id@A
>>notation superfluous.
>>    
>>
>
>But this does mean that one of your two theorems will be modified a bit if
>you use the new notation:
>
><A,id@A> = id@inv(A)
>
>It's true that this can be inferred, but it's confusing.
>
Yep, you're right, this is confusing, and also both id != id and id = id
being true, depending on the context of the id patches.

So I guess when using identity patches, we should always make the
context explicit.  BTW, if anyone has a better notation, feel free. 
(Perhaps a typing-like double-colon notation: id::A ?)

To make explicit the reasoning that you used above: in <A,id> both sides
have the same context, so the right hand side is id@A.  And the context
of the left hand side of the equation <A,...> is inv(A), so the right
hand side of the equation is id@inv(A).  The last step uses

    <A,B> || inv(A)           "axiom: context of <,>"

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]