> >> 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 _______________________________________________ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
