Re: How to extend a patch theory to fully commute

On Thu, 2 Jul 2020 at 09:42, Ben Franksen <[email protected]> wrote:
> 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.

Good idea. https://hub.darcs.net/falsifian/misc-pub/patch/8b55486b825568be209028b994383274a85ec1f3#misc/hms_patchfinder

> 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).

I agree with your suspicion. I have at least the start of an idea for
implementing this reasonably efficiently, but I need to think more
about it.

James