[Iris-Club] Cancellativity of RA

[Dan Frumin]

Hi Zhen,

I don’t actually thin that Calcagno and O’Hearn use the fact that a separation algebra is cancellative.
IIRC they only need that P(\Sigma) is a (boolean) BI-algebra whenever \Sigma is a separation algebra. And for that you don’t need cancellativity.
Similarly, in Iris one can construct a (intuitionistic) BI-algebra from a RA.

I think that the business with precise predicates makes more sense in non-intuitionitic separation logic, because in Iris assertions are upwards closed.

Best,
Dan

> On 09 Mar 2017, at 10:23, Zhen Zhang <zhangz at mpi-sws.org> 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
> 
> -- 
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org