[Iris-Club] Cancellativity of RA

[Ralf Jung]

Hi,

> 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.

Indeed we no longer need cancellativity for the auth updates; we found a
weaker but still sufficient condition.  As Robbert already mentioned,
cancellativity is still "good enough" for local updates, as witnessed by
cancel_local_update.

> Also, for
> certain instantiation of RA, like gmap, it looks like cancellativity is
> implied even though not required to be a CMRA.

I am not sure I understand.  Are you saying that some of our CMRAs are
cancellative?  Sure.  Just like some are positive, for example.

> 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?

That's a good question, I do not know if there is a "deep" reason for
why they need things to be cancellative.  Notice however that if
anything, separation algebras make reasoning *weaker* because they
*have* to be cancellative.  If we stumble upon something that only works
for cancellative RAs, we can always locally require the RA in question
to be cancellative, without forcing this to be true for all RAs.
  The same is btw true for another restriction present in separation
algebras that we did not have to make:  If you look at their rules for
the "duplicable core", you will see that they require the core to
commute with composition, i.e., it has to be a homomorphism.  The core
of an RA just has to be a monotone function.  This is important for us
because we actually have an RA with a core that is *not* a homomorphism
(namely, the RA for state-transition systems).  Again this means we can
write down more RAs.

Kind regards,
Ralf