coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Cumulatively of Universes
- Date: Mon, 13 Mar 2017 18:04:27 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f42.google.com
- Ironport-phdr: 9a23:FlNPThILFqCz+PJ8qNmcpTZWNBhigK39O0sv0rFitYgeKfjxwZ3uMQTl6Ol3ixeRBMOAuq8C1rad6vi/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT69bL9oLBi7ogrdutQKjYZgN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhTwZPDAl7m7Yls1wjLpaoB2/oRx/35XUa5yROPZnY6/RYc8WSW9HU81MVSJOH5m8YpMAAOoPP+lWr4fzqVgToxWgGQahH/ngxiNSi3LswaE2z+YsHAfb1wIgBdIOt3HUoc30OqcIT++1w67IzS/DbvhL3jny8ozIfQ49rvGMR717bM3cyUYqFwzfilWft5DqPzOP2ekWvGib6vBvVeOri2I9tw5xpT2vy94qh4LUiIwVzVXE+j94wIYzPdC3UlR7bsKkEJtRqSGVKZB2TtolQ2F1piY11KcGuYKlcygR0pgnyQTfZ+SIc4iJ/hLjVPuRLixiiHJkf7KygQu5/0u4yuDkSMW4zFJHojBGn9TMrHwByQHf58adRvZy4Eus3yuE2RrJ5eFeO080kLLWK54/zb40kZoeqUHDETX3mEXylaOWaEYk9vSx5+TpbbjquIWQN4BzigH5PaQuntKwDf4kPQgJWmiX4eW81Lv98k3lWLhGkOE6n63DvJ3ZJckXvLC1DxJb34o55BuzES+q0NECknkGKFJFdgiHj4/sO1zWL/D4CO2wg1Cynzh3x/DJJKbsAprILnfZkbfheaxx5FJbyAo21dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zHQaZOGC2YYdICSzGe0jKEGEa1LthM0AGCEEpFxtYvbtjQitSzNcYGyjF4c14jwwCIvuWYjGT4Sgi7yI9Ci+F5xSIGtBDwbfQj/Ta4yYVqJUO2qpKch7n2lBDOD5Rg==
All of this is great information. Thanks!
On Mon, Mar 13, 2017, 11:15 AM Matthieu Sozeau <mattam AT mattam.org> wrote:
Hi all,Indeed it is less useful in presence of polymorphism, but not completely useless still,if it can go through inductive types (examples in the work of Timany on a category theorylibrary suggest that). Ali Assaf's thesis is indeed the most up-to-date comparison for universeswith and without cumulativity I think. I think there is an advantage of cumulativity in the presence ofpolymorphism (or just lots of universes) regarding unifying universe expressions, which are relegatedto the constraint inference engine. E.g. you don't get into problems like max(i,j) =? max(i',j') that haveno canonical solutions but instead get two fresh universes l and l' representing these two lubs and l = l'.Best,-- MatthieuOn Mon, Mar 13, 2017 at 3:57 PM Bas Spitters <b.a.w.spitters AT gmail.com> wrote:Interestingly, the lean developers (in CC) have decided against
cumulative universes.
IIRC cumulativity complicates the implementation and the meta-theory,
but *in the presence of universe polymorphism* it does not add much
extra convenience.
Unfortunately, I cannot find a discussion of the rationale, but
someone will fill us in, I hope.
On Mon, Mar 13, 2017 at 3:00 PM, Frédéric Blanqui
<frederic.blanqui AT inria.fr> wrote:
> Hi Grégory, you may be interested in Ali Assaf's PhD thesis:
> https://pastel.archives-ouvertes.fr/tel-01235303v4 .
>
>
> Le 03/13/2017 à 02:51 PM, Gregory Malecha a écrit :
>
> Hi, Coq-Club --
>
> I'm wondering if anyone can point me to literature related to cumulatively
> vs. non-cumulatibity of universes. My vague understanding is that
> cumulatively offers no additional power but that there are some things that
> are easier to express with cumulative universes (in particular you can avoid
> resizing in terms). Cobstructivwly, I would expect such a result to give a
> translation from a world with cumulative universes to one without them. A
> paper on that topic would be particularly interesting to me.
>
> Thanks in advance for any pointers.
> --
>
> - gregory malecha
> gmalecha.github.io
>
>
--
- gregory malecha
gmalecha.github.io
- [Coq-Club] Cumulatively of Universes, Gregory Malecha, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Frédéric Blanqui, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Bas Spitters, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Matthieu Sozeau, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Gregory Malecha, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Matthieu Sozeau, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Jason Gross, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Bas Spitters, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Frédéric Blanqui, 03/13/2017
Archive powered by MHonArc 2.6.18.