[Iris-Club] Cancellativity of RA

[Zhen Zhang]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20170309/1ca6d495/attachment.html>