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

[Ben Franksen]

Am 01.07.20 um 05:09 schrieb James Cook:
> Definition: We associate a primitive context to every context address
> (and in particular to every extended context) (a, b, (Qi), X, Y) using
> the following recursive algorithm.
> 
> * If X=Y={}, then the context is a (=b). This is an embedded primitive
> context.
> 
> * If the sequence (Qi) can be permuted so that it starts with a patch P
> in X, then we recurse on (a', b, (Q'i), X \ {P}, Y), where a' is ending
> context of P and Q'i is the rest of the sequence.
> 
> * Similarly, if (Qi) can be permuted so that it ends with a patch P in
> Y, then we recurse on (a, b', (Q'i), X, Y \ {P}), where b' is the
> starting context of P and (Q'i) is the rest of the sequence.
> 
> * Otherwise, we have a minimal context address. Swap X and Y and recurse
> on the result (a, b, (Qi), Y, X).

As a possible simplification, wouldn't it be enough to define the
associated primitive context for minimal context addresses? This would
eliminate the second and third case. The fourth case would be
re-formulated as

* Otherwise swap X and Y, minimize, and recurse on the result.

It is clear that a minimal context address is no longer minimal if we
swap X and Y. Thus, the minimization actually makes it "smaller" ( i.e.
(Qi) becomes shorter), proving termination.

In general, I think it would be good to dwell a bit on this minimization
process early on. That is, given some arbitrary context address, how
exactly do we calculate a minimal version? I suspect this will be (at
least) quadratic in the length of the context address (see my earlier
remarks about calculating minimal contexts).

Cheers
Ben