[Iris-Club] CMRA structure on uPred

Ralf Jung jung at mpi-sws.org
Mon Oct 10 21:29:42 CEST 2016


On 29.09.2016 22:30, Robbert Krebbers wrote:
> The proper way of dealing with big operators is to define them in terms
> of a canonical structure for monoids. However, I rather keep the
> algebraic hierarchy as small as possible, and define the big operators
> in terms of CMRAs with units (even if that may be considered an
> engineering hack).

This could be entirely separate from the algebraic hierarchy, and not
increase it at all. (I think I saw this proposed somewhere, but can't
find the source now, so here I'm just echoing someone else.)  I don't
see a good reason why everything you compose with bigops should have a
core and validity, and there are some things you can do already with
just associativity -- tying this to RAs seems rather silly, and even
prevents us from also doing e.g. bigops on conjunction.

Kind regards,

More information about the Iris-Club mailing list