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

List:       darcs-conflicts
Subject:    Re: [darcs-conflicts] permutivity,
From:       David Roundy <droundy () abridgegame ! org>
Date:       2005-11-04 13:30:32
Message-ID: 20051104133023.GK25996 () abridgegame ! org
[Download RAW message or body]

On Mon, Oct 31, 2005 at 08:04:05PM +0000, Ian Lynagh wrote:
> On Mon, Oct 24, 2005 at 09:44:32AM -0400, David Roundy wrote:
> > 
> >                                 I'm going with a new notation for
> > conflictors, which looks like
> > 
> > [A1:,A2:,A3:A2...|Pre:P:Post|:B1,:B2,B2:B3,...]
> 
> We haven't had a new conflictor definition for /far/ too long, so I'll
> be using
> 
> [Es; {Pres}; PrePs:P:PostPs; {Posts}]
> 
> where Es is the effect, Pres and Posts are sets of conflicts (with pre
> and post contexts respectively), P is the patch and PrePs/PostPs are
> pre/post context of P. Simple, ain't it?  :-)

I don't think so.  It seems to me that it's got way too much redundancy,
and that this will complicate our code too much.

> In Haskellish notation that is
> 
> Conflictor a c = Conflictor (PatchSeq a c)           -- Es
>                             [PatchWithPreContext a]  -- Pres
>                             (PatchSeq a x)           -- PrePs
>                             Patch x z                -- P
>                             (PatchSeq z c)           -- PostPs
>                             [PatchWithPostContext c] -- Posts

Here Es is equal to (PrePs P PostPs), so I'd say that for purposes of the
formalism we can just leave Es out of the picture? Yes, it might be a good
idea to store in simplified form as an optimization, but for purposes of
reasoning about conflictors it seems irrelevant.

[...]
> This is largely the same as yours but I hope with more useful contexts.

The big difference is that your PrePs and PostPs are very differently
defined than mine.  In particular, they don't seem to have a well-defined
meaning.  My Pre and Post were always patches that hadn't conflicted with
P, but which had conflicted with something that conflicted with P.  Your
PrePs and PostPs are either P^, or my Pre/Post or the inverse of my
Pre/Post, or some of the patches we conflict with.  My format had the
feature that any given patch will show up exactly once (except as the
context of one of the other A1,A2,B1,B2, etc), so when commuting we only
need to search for a given patch in one place.

> > At last... permutivity tells us that for a sequence of patches A1B1C1, all
> > permutations can be represented by
> > 
> >      A1 B1 C1
> > <->* B2 A2 C1
> > <->* B2 C2 A3
> > <->* C3 B3 A3
> > <->* C3 A4 B4
> > <->* A1 C4 B4
> 
> Or equivalently,
> 
>        A1 B1 C1
> <-AB-> B2 A2 C1
> <-AC-> B2 C2 A3
> <-BC-> C3 B3 A3
> <-BA-> C3 A4 B4
> <-CA-> A1 C4 B4
> 
> > The simplest scenario is A1B1C1 == ABC, and none of these patches commute.
> > In this case
> > 
> > A1 = A ~ A
> > B1 = B ~ B
> > C1 = C ~ C
> > B2 = [A:|:B:|] ~ A
> > A2 = [|:A:|:B] ~ B
> > B4 = [|:B:|:C] ~ C
> > C4 = [B:|:C:|] ~ B (easy so far)
> > C3 = [A:B,B:|:C:|] ~ AB
> > A3 = [|:A:|:B,B:C] ~ BC (these two are also old friends)
> > A4 = [|:A:B|:C] ~ id (id means identity)
> > C2 = [A:|B:C:|] ~ id (another pair of old friends)
> > B3 = [A:|:B:|:C] ~ B^ (!!! this is Ian's conflictor, remember ^ is inverse)
> 
> Using the above patch effects gives me:
> 
>        ABC
> <-AB-> [A; {}; A:B:B^; {A:}][B; {:B}; A^:A:B; {}]C
> <-AC-> [A; {}; A:B:B^; {A:}][; {}; B:C:C^B^; {A:}][BC; {:B,B:C}; A^:A:BC; {}]
> <-BC-> [AB;{};AB:C:C^;{A:B,B:}][B^;{:C};B^:B:B^;{A:}][BC;{:B,B:C};A^:A:BC;{}]
> <-BA-> [AB; {}; AB:C:C^; {A:B,B:}][; {:C}; B^A^:A:B; {}][C; {:C}; B^:B:C; {}]
> <-CA-> A[B; {}; B:C:C^; {B:}][C; {:C}; B^:B:C; {}]

I don't like how

AB <-> [A; {}; A:B:B^; {A:}][B; {:B}; A^:A:B; {}]

Even leaving out the Es, still each patch shows up twice.  There are
multipatch constraints on the validity of a given conflictor.  If I have a
conflictor (leaving out Es)

[{:M}; N:P:O; {}]

then it must be true that M == O and N == P^.  So what do we gain from
storing these extra copies?  We gain some simplicity in the conflictor
data format, since it has one constructor and the contexts are all easily
known, but at the cost of redundancy in the format, which means that the
format will support more complexly-wrong (yes, I know that's not a word)
invalid patches, and figuring out whether our algorithm works on all
*valid* patches will be accordingly more difficult.  Note that there's also
the constraint that the pair of patches OP do not commute (which I believe
is unavoidable).

The only alternative I can think of (which I think I may have hinted at,
although maybe I just thought about hinting at it) is to have separate
constructors for different special cases of conflictors.  So in my notation

AB <-> [A:|:B:|][|:A:|:B]

these would have a constructor like (pretending that Autrijus has finished
his GADT record fields patch, and that I knew what the syntax was):

data Conflictor _ _ =
  Conflictor o a :: C1 { -- for [A:|:B:|] (I haven't thought of a name)
                      effect :: PatchSeq o a,
                      prestuff :: [PatchWithPostContext a],
                      thepatch :: Patch a b
                    }
  Conflictor a b :: C2 { -- for [|:A:|:B]
                      effect :: PatchSeq a b,
                      thepatch :: Patch o a
                      poststuff :: [PatchWithPreContext a],
                    }

Note that I've still got both a redundancy and a constraint, which are that
the effect must be the result of merging all the prestuff or poststuff,
respectively.  This is annoying.  I suppose one could remove the redundancy
by defining something like:

data Conflictor _ _ =
  Conflictor o a :: C1 { -- for [A:|:B:|] (I haven't thought of a name)
                      preeffect :: PatchSeq o a,
                      thepatch :: Patch a b
                    }
  Conflictor a b :: C2 { -- for [|:A:|:B]
                      thepatch :: Patch o a
                      posteffect :: PatchSeq a b,
                    }

where the patches in the preeffect and posteffect represent all the patches
that would have been in the prestuff and poststuff.  This works as long as
none of them conflict.  If some conflict, though, then we're looking at a
more complicated merge, and that'll take some more thought.

Basically, my idea is to replace what in your representation would be a
check for empty sequences and empty lists (followed by a possible assertion
that M == O and N == P^) with a match against a different constructor.
This seems like it might be more robust.  The question would be how many
such constructors one needs.  I think I argued to myself that you'd need at
least four (these two, plus one that for identity patches and one for
patches that are equivalent to P^).  If these four really are sufficient,
then I think this would be the way to go.  (Also, I'd have to be able to
figure out appropriate contexts for the identity case...)
-- 
David Roundy
http://www.darcs.net

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