On Tue, Jan 26, 2021 at 08:49:30PM +0100, Ben Franksen wrote:
> Am 24.01.21 um 12:03 schrieb Ben Franksen:
> > A /realization functor/ R is a functor from abstract patches (sequences
> > of names and contexts) to concrete patches (with a commute function),
> > such that
> >
> > (a) R maps abstract paths to concrete paths of the same length
> > (b) for any two parallel abstract paths ns and ms of length 2,
> > commute(R(ns))=Just(R(ms)) (here R is the mapping on arrows)
> > (c) there is a distinguished state E, such that E is an element of
> > R({}) (here R is the mapping on objects i.e. contexts)
This seems reasonable. For (b) I guess you mean any two /different/
paths of length 2?
> I just realized (pun, haha) that this functor has a name in Darcs: we
> call it 'effect'. I think I like that name better.
>
> Here is my picture of the overall structure of patch theory, when
> extended to the lower levels. We have three categories: abstract patches
> (AP), concrete patches (CP), and partial bijections (PB), and two functors:
>
> AP ---effect--> CP ---apply--> PB
>
> (While PB is a groupoid, CP is not, contrary to what I stated in my last
> mail, because that would mean pp^:s->s = id_s, which does not play well
> with commutation).
>
> The effect functor is understood to be relative to some choice of start
> state, see condition (c). Neither functor is injective (on morphisms;
> for objects I haven't checked this). I don't think the apply functor is
> surjective in any strict sense, but we should reasonably expect that for
> any two states s and t there is an arrow p in CP such that apply(p) is
> defined at s and apply(p)(s)=t. Indeed, the treeDiff function in Darcs
> gives a possible solution (the result depends on which diff algorithm is
> selected).
Thanks, this clears things up a bit for me. I hadn't realized you meant
CP and PB to be different, which might explain my confusion about
"patch theories that violate (b)" from my previous email.
One nitpick: the definition of "sensible" in the inverse semigroup
paper might be different from yours and from the Camp definition.
Definition 1.8 says a patch is sensible if it's effect isn't "0", which
I think just means its domain and range are nonempty.
Let me check my understanding of the picture you've painted:
* A "patch theory" or maybe "implemented patch theory" is a tuple
(State, Name, E, AP, CP, PB, commute, effect, apply) satisfying all
the following conditions.
* State and Name are sets, intended to denote the set of possible
states and names respectively. (E.g. type State = [Char] in your Jan
24 email.)
* E is an element of State: the "starting state".
* AP we've discussed a fair bit. It is a category. Its objects are
subsets of Name, its morphisms are labelled with sequences of names,
and we've previously listed some axioms AP must satisfy.
* PB: the objects are all possible subsets of State, and the morphisms
between any two objects are all possible bijections between those
sets. (PB is fully determined by the set State, so it could be left
out of the tuple defining the patch theory.)
* CP I'm less sure about. I guess it is any category whose objects are
the same as PB's objects. There are no constraints on its morphisms
other than what will be implied by our requirements on the effect
functor.
As a concrete example, in your toy patch theory, the morphisms in CP
between any objects S and T are triples (S, T, e) where e is an
element of [PrimPatch] for which apply(e)(S) = T (applying a function
to a set in the natural way). I include S and T as part of the
morphism so that the same e can appear in different morphisms.
Concatenating two morphisms (S, T, e) and (T, U, f) produces (S, U, e
++ f). The identity on S is (S, S, []).
* commute is a partial function on length-two paths in AP. (Maybe
"commute" could be out of the tuple, and instead be implied by the
effect functor. I haven't checked that this makes sense.)
* effect : AP -> CP is a functor satisfying the properties (a), (b) (c)
from your Jan 24 email ("realization functor").
* apply : CP -> PB is any functor.
Introducing conflictors to such a patch theory would mean the
following:
* Extending AP so the set of objects ("contexts") is closed under
union.
* Adding new morphisms to CP, called "conflictors".
* Extending the effect functor so it's defined on the newly expanded
AP, probably using the "conflictor" morphisms added in the previous
step.
* Extending the apply functor so it's defined on the morphisms
(conflictors) added to CP.
The first is a deterministic change; no decisions are required. The
rest requires careful design.
> The effect functor is surjective only if we restrict CP to sequences
> that are "sensible" relative to the chosen start state. For any sensible
> concrete patch sequence cp there is a sequence of names ap such that
> effect(ap)=cp, since this is precisely the condition under which we are
> able to record such a sequence.
That's an interesting statement. Giving names to patches seems a bit
tricky to reason about. I guess if we pretend that when Darcs makes up
a random name for a patch, it's actually "discovering" a previously
unknown mapping under some predetermined but inaccessible effect
functor, then what you're saying should be true. I hope that makes
sense. I don't know if there's a better way to look at it.
--
James
_______________________________________________
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
