[darcs-devel] Right and left inverses

[David Roundy]

On Fri, Mar 28, 2008 at 06:17:33PM +0100, Jules Colding wrote:
> 
> On 28/03/2008, at 15.16, David Roundy wrote:
> >On Thu, Mar 27, 2008 at 09:56:18PM +0100, Jules Colding wrote:
> >>I'm still reading appendix A in the darcs2 manual. Right after  
> >>theorem
> >>1 it is said that:
> >
> >Perhaps I should belatedly warn you that the appendix A is in need of
> >considerable work...
> 
> Thank you for the warning ;-)
> 
> Appendix A seemed to me the best place to start if I wanted to  
> understand the theory behind darcs, which I do. Any update/rewrite  
> planned?

It's still probably to start, but just keep in mind that some of it may be
incorrect or obsolete, and you probably want to ignore just about all the
stuff about conflicts (or read it for historical interest).  Jason Dagit
wrote up a little paper this summer, which has some more up-to-date
description, but is still obsolete.  I want to write a new description of
darcs' semantics, but am not sure when (if ever) that'll happen.  It may be
that Jason's thesis will serve as the kernel for a paper on this.

> >>	"it is possible to show that the right inverse of a patch is equal  
> >>to
> >>its left inverse"
> >>
> >>How?
> >
> >You simply consider the inverse of the inverse.  If the inverse of the
> >inverse is the original patch, then the right inverse is the same as  
> >the
> >left inverse.
> >
> >let riA = right-invert A
> >
> >which means that
> >
> > A riA has same effect as the identity change
> >
> >let liA = left-invert A
> >
> >means that
> >
> > liA A has the same effect as the identity change
> >
> >So now consider
> >
> >rrA = right-invert riA
> >
> >so riA rrA has the same effect as identity
> >
> >Now if rrA is the same as A, we conclude that riA == liA.
> 
> 
> OK, in other words:
> 
> riA rrA = I, I is the identity change

Well, we need to be careful with equality in this case, since you certainly
can't insert riA rrA anywhere you could insert I, so they aren't equal for
any normal definition of equal.  But taken with that caveat, yes.

> A riA = I
> => A riA rrA = rrA
> => A I = rrA
> => A = rrA

No, this isn't a good idea.  We can't substitute like this without extreme
care.  There is a fundamental difference between A riA and I, which is that
they commute differently, and why we can only say that they have the same
effect.

> now substituting into riA rrA = I we get:
> 
> riA A = I
> => riA = liA

No, we don't want to substitute things in like this, as it's not really
safe (or perhaps I should say that the operation isn't well-defined... or
that this is a limitation on what we mean by "A riA = I").

> The only assumption I can see that is made underway is that:
> 
> IA = AI = A, where I is the identity change.
> 
> which seems logically valid although I'm not sure a mathematician  
> would agree without a rigorous proof.
>
> >So I've shown that the statement you were asking about right/left
> >inverse equality is the same as the statement that the right-invert (or
> >alternatively left-invert) is a self-inverting function.
> 
> Yes.
> 
> 
> >So how do we know that inversion is self-inverting? That comes from the
> >effect of identity.
> >
> >If we begin in state o, then applying A gives us state a.  Then applying
> >riA gives us the state o.  Applying rrA must give us the state a again
> >(since it's the right-invert of riA), and the patch that takes us from o
> >to a is A.
> 
> In  other words:
> 
> A o  --> a
> => A riA o --> o
> => A riA rrA o = A o --> a
> 
> substituting (A riA = I) now gives:
> 
> rrA o --> a
> => rrA = A
> 
> The same can be done for llA. I'm sorry if my notation isn't correct,  
> but the meaning should be clear.

Yes, this sounds right.  And it's a safer statement of the first bit you
said above, which I objected to.  In this case the assumption is explicit:
we assume that if two patches have the same effect, then they are the same
patch.  I objected above that this is not true, that A riA is not the same
as I, because they commute differently, so we need a bit more caution
here.  If two *primitive* patches have the same effect, then they are
identical patches.  This is true, provided we're willing to define "effect"
in a generic sense, such that the effect of a replace patch that affects
only one line of a file is acknowledged to be different from the effect of
a hunk patch that changes the file in precisely the same manner.  This is
a subtle question, as the only difference between these two changes
involves how they would affect *other* files... or how they commute.
-- 
David Roundy
Department of Physics
Oregon State University