[prev in list] [next in list] [prev in thread] [next in thread] 

List:       darcs-devel
Subject:    Re: [darcs-devel] Semantics of witnesses
From:       Benjamin Franksen <ben.franksen () online ! de>
Date:       2019-08-29 12:01:59
Message-ID: qk8ern$77jf$1 () blaine ! gmane ! org
[Download RAW message or body]

Am 29.08.19 um 11:21 schrieb Ganesh Sittampalam:
> On 29/08/2019 08:35, Ben Franksen wrote:
>> I wonder if the minimal context idea could be adapted to set (2). All we
>> need to do is check that, after commuting, our patches are structurally
>> equal to the input patches.
>>
>> This is currently just a theoretical consideration.
>>
>> To avoid ambiguities about what exactly structural equality means for
>> compound patches we could define new operations that are like commute
>> but fail if the commute isn't trivial. We need to distinguish whether we
>> want this property for the left or the right patch, so we'd add two new
>> methods:
>>
>>   trivialCommuteL :: CommuteFn p p
>>   trivialCommuteR :: CommuteFn p p
>>
>> Building on these, and the regular commute, define
>>
>>   trivialCommuteWhatWeCanRL :: <same type as commuteWhatWeCanRL>
>>
>> to minimize any concrete given contex.
>>
>> However, for this to be useful we'd have to know if trivialCommuteR
>> satisfies enough patch laws; in particular, we'd need permutivity for
>> trivialCommuteR and I am not sure it holds even for Prim.V1.
> 
> The asymmetry between trivialCommuteL and trivialCommuteR would probably
> significantly complicate the theory, as now there isn't a single
> self-inverse commute operation but two operations that are inverses of
> each other.
> 
> Also, this would be restricted to contexts you can get to directly. For
> example if p;q commute but q changes representation, then in the
> sequences q and p;p^;q , q has the same representation but you can't get
> from one to the other.

Hm, yes. It's what I feared: these operations aren't well-behaved enough
to be useful.

Cheers
Ben

_______________________________________________
darcs-devel mailing list
darcs-devel@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-devel
[prev in list] [next in list] [prev in thread] [next in thread]