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