[Iris-Club] Several small questions on Iris

Ralf Jung jung at mpi-sws.org
Thu Feb 16 10:25:12 CET 2017


Hi,

>     Wait, wasn't the entire point of your proposal that no list of CMRAs
>     needs to be given?  You wrote "why don't you just product over all
>     possible bifunctor \Sigma?"
>     If by that you mean "all bifunctor \Sigma given in a list", then I don't
>     understand the question.  That's pretty much what we are doing,
>     isn't it?
> 
> 
> Yes, I meant "all bifunctor \Sigma", not "... given in a list".  I just
> wanted to product over all possible \Sigma.  My idea is, anyway you
> already restricted the sizes of the CMRAs by mentioning the list of
> them, so why not just producting over all CMRAs with *that size* you
> used in the list?

Sorry, I don't understand what you mean by this.  Maybe there is a
confusion about the term "size"?  Note that "size" does not mean
"cardinality". The "size" here corresponds roughly to a universe level
in Coq.  Currently, all CMRAs we have are of the same size because the
type cmraT exists in a particular universe (picked by Coq).  If we tried
to write down the CMRA of all CMRAs, that would be a size violation and
Coq would detect that as a universe inconsistency.  The underlying
reason for this is that the CMRA of all CMRAs would itself be a CMRA and
hence included in the set of all CMRAs that it is taking a product over
-- which, if allowed, would lead to a Russel-style paradox.

We currently do not have CMRAs of different sizes; doing so would
require using Coq's universe polymorphism to have a CMRA structure for
every universe that can contain CMRAs of lower universes.  I guess if we
did that we could parameterize all our proofs by the universe level that
is used for the "big product", making all lower universes available for
the user-supplied CMRAs.  Combining different proofs would use the
maximum universe.
  That could work, but (a) it's very different from what you suggested
[so it doesn't help me understand your question], and (b) messing with
Coq's universe polymorphism like that sounds very daring and asking for
trouble. ;)

Kind regards,
Ralf



More information about the Iris-Club mailing list