coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vincent <vincent.siles AT gmail.com>
- To: Dan Doel <dan.doel AT gmail.com>
- Cc: Vladimir Voevodsky <vladimir AT ias.edu>, homotopytypetheory AT googlegroups.com, Coq-Club Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] pure type systems (Barendregt)
- Date: Fri, 17 Jun 2011 07:49:58 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=uQWsOUZgtt3k4fFJsRIvrlo4pCEu1zinz5ju0+9jWa41+RGIBt8fQlB/+HIWlF87C+ /16S/IqK8khLOKZSE+KXCx0/fuCiNbWJRA/EZxWiwIXP7dsrY2kMig6Uz1QRW8yshhiW te4ijJEOfkWiLwaByd6rdqs7+XqXyQxdBnwqk=
I forgot to point out that Bruno Barras did lots of formalization
about PTS, and one of them has abstract subtyping.
Take a look here for the Coq files:
http://pauillac.inria.fr/~barras/coq_work-eng.html
Cheers,
Vincent
2011/6/17 Dan Doel
<dan.doel AT gmail.com>:
> On Thu, Jun 16, 2011 at 5:55 PM, Vladimir Voevodsky
>Â <vladimir AT ias.edu>
> wrote:
>> I have been looking at Barendregt's "Lambda calculi with Types" and I have
>> the following question. It seems that he is considering systems with
>> different universe arrangements but he never assumes one universe to be a
>> sub-universe of another. Is it so or am I missing something? And if this
>> is so is there a careful analysis of the analog of PST's where universes
>> are not only members but also subtypes of each other?
>
> At least as far as universes go, there is sort of a way around needing
> subtyping in pure type systems, although I must admit I completely
> overlooked it myself for quite some time.
>
> The crux is that the 'axioms' and the 'rules' (assuming I'm using the
> standard terms) needn't be functional relations. So, you can get
> cumulativity via axiom/rule sets like:
>
> (Type0, Type1)
> (Type0, Type2)
> ...
>
> (Type0, Type0, Type0)
> (Type0, Type0, Type1)
> ...
>
> Essentially, you add a rule for every possible way cumulativity could be
> used.
>
> The problem with 'non-functional' pure type systems like these is that
> checking tends to become semi-decidable. You may eventually find a
> correct choice of axioms/rules for a particular term, but you can
> never get through all of them to definitively say that certain terms
> are ill-typed. By contrast, 'functional' pure type systems admit
> decidable checking/inference of sufficiently annotated terms.
>
> The boon of the cumulativity/subtyping approach, like Luo's, is that
> terms admit principal types, and there is an algorithm for deciding
> them. Essentially, it is a slightly different treatment of a special
> case of the general class of non-functional pure type systems that
> admits decidable checking.
>
> As for reading about systems with cumulativity, I recommend Luo, as others
> have.
>
> -- Dan
>
>
- [Coq-Club] pure type systems (Barendregt), Vladimir Voevodsky
- Re: [Coq-Club] pure type systems (Barendregt), Vincent Siles
- [Coq-Club] Re: [HoTT] pure type systems (Barendregt),
Robert Harper
- Re: [Coq-Club] Re: [HoTT] pure type systems (Barendregt), Randy Pollack
- Re: [Coq-Club] pure type systems (Barendregt), Matthieu Sozeau
- Re: [Coq-Club] pure type systems (Barendregt), Frederic Blanqui
- Re: [Coq-Club] pure type systems (Barendregt),
Dan Doel
- Re: [Coq-Club] pure type systems (Barendregt), Vincent
Archive powered by MhonArc 2.6.16.