[darcs-users] How to extend a patch theory to fully commute

[James Cook]

> >> A good way to see if your definition holds up is to see whether you can
> >> prove your
> >>
> >> Conjecture 1: Every context address points to at most one context.
> >
> > Sure, that's a nice goal.
> >
> > I think I will start a latex file, try to define what a patch theory
> > is and what context address is for a given patch theory, then try to
> > prove Conjecture 1.
> >
> > I know of two places with formal definitions of "patch theory": J.
> > Jacobson's Inverse Semigroups paper and the Camp theory document. I'll
> > probably start a new definition with just the properties I find I
> > need. (A patch theory is a (possibly infinite) directed graph, with a
> > "commute" relation and a "name" function, satisfying the following
> > axioms: ...)
>
> I think the approach you took so far is better: find out bit by bit what
> you need, instead of trying to come up with a full formal definition up
> front.

Okay, I wrote something up: https://www.falsifian.org/a/xxOw/misc.pdf
; Latex source at
https://hub.darcs.net/falsifian/misc-pub/browse/patch_theory/misc.tex

This covers just the definition of "patch universe" and Conjecture 1
(every context address points to at most one context).

I ended up going in an unconventional direction: patch commuting is
not fundamental to my definition of a "patch universe" but instead can
be derived from it (proofs in Sec 2.3). There are two reasons I went
this way:

(a) it's simple: a patch universe is a just graph with names on the
edges, and the rule that if you follow a sequence of edges where the
names "balance out", you end up back where you started.

(b) It makes my Conjecture 1 easy to prove. (In other words: I
cheated. Hopefully I haven't optimised for this use case too
narrowly...) See Section 3. I changed the definition of Context
Address to work better with my new "patch universe" definition, but I
think it amounts to the same thing.

The terminology is kind of dense right now and the write-up could
benefit from examples. If you prefer, you could wait until I've done
some more work on it. (I might discover bugs in the meantime too.)

James