[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