[Iris-Club] Cancellativity of RA

[Robbert Krebbers]

Hi Zhen,

the cancellation property is not an axiom simply because many of the RA 
constructions do not enjoy the cancellation property. For example, 
consider the RA of sets with union as the operation:

   we have { 1 } ∪ { 1 } = { 1 } ∪ ∅
   but not { 1 } = ∅

Apart from this, there are plenty of other RAs that do not enjoy the 
cancellation property.

Since a while ago we have the notion of cancelable elements in the Coq 
formalization of Iris though:

   Class Cancelable {A : cmraT} (x : A) :=
     cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.

Which enables the following local update:

    Lemma cancel_local_update x y z `{!Cancelable x} :
      (x ⋅ y, x ⋅ z) ~l~> (y, z).

See also https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/43

Robbert

On 03/09/2017 10:23 AM, Zhen Zhang wrote:
> Hi all,
>
> I wonder why in current definition of RA, cancellativity is not
> required as an axiom?
>
> I noticed that in Iris 1.0, authoritative monoid AUTH(M) requires M
> to be cancellative to support the AUTHUPD rule. But in Iris 3.0, with
> local update as a condition of a more general auth update rule, the
> cancellativity requirement is also (seemingly) dropped. Also, for
> certain instantiation of RA, like gmap, it looks like cancellativity
> is implied even though not required to be a CMRA.
>
> In “Local Action and Abstract Separation Logic”, the “Separation
> Algebra” requires cancellativity to support his program logic (which
> I am not familiar with). I wonder if it has anything to do with local
> reasoning and precise assertions? Will our non-cancellative RA be too
> weak to support certain reasoning like this?
>
> Thanks, Zhen
>
>
>
>