[Iris-Club] Cancellativity of RA
Robbert Krebbers
mail at robbertkrebbers.nl
Thu Mar 9 10:35:08 CET 2017
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
>
>
>
>
More information about the Iris-Club
mailing list