Re: How to extend a patch theory to fully commute

Am 01.07.20 um 17:59 schrieb Ben Franksen:
> Am 01.07.20 um 17:13 schrieb James Cook:
>> On Wed, 1 Jul 2020 at 10:21, Ben Franksen <[email protected]> wrote:
>>> Am 01.07.20 um 05:09 schrieb James Cook:
>>>> The context address /points to/ a context c if there exists a
>>>> permutation of (Qi) such that all the patches with names in X come
>>>> before patches with names in Y, and c is the after-context of the k-th
>>>> patch in the sequence (equivalently, the before-context of the (k+1)-th
>>>> patch), where k = |X|.
>>>
>>> and later:
>>>
>>>> Definition: A context address (a, b, (Qi), X, Y) is /minimal/ if it is
>>>> impossible (in the primitive patch theory) to commute the sequence (Qi)
>>>> so that it begins with a patch in X or ends with a patch in Y.
>>>
>>> Did you mix up X and Y here? I would have expected the sentence to say
>>> "begins with a patch in Y or ends with a patch in X".
>>
>> I think this part is correct as written. I added some more
>> explanation: https://hub.darcs.net/falsifian/misc-pub/patch/3bf868962261b8b275f81a82136106ee4c444dd1
>>
>> The point of minimal addresses is that they "point" to contexts that
>> aren't already part of the primitive patch theory. If a patch in X
>> could be moved to the start, or a patch in Y could be moved to the
>> end, then the address could be made even more minimal by leaving out
>> that patch (the more minimal address would be called a
>> "simplification" as defined in Chapter 4).
> 
> Okay, I think I got it now. Thanks for the explanation.

Just to check I understood the idea (up to this point): roughly
speaking, you represent "unrepresentable" states by formally commuting
patches.

That is, if we regard the primitive states as vertices and primitive
(named) patches as edges in a graph, then you extend the graph with new
nodes and edges.

The construction works by inductively taking any pair of incommutable
patches (in sequence, i.e. with a common middle state) and then
"formally" commuting it. The new node is represented as that pair of
patches. Is that, essentially, the idea?

It reminds me of the darcs-1 patch format, where a "merger" patch is
defined as the ordered pair consisting of both conflicting patches.

Cheers
Ben