The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

> If you try to formulate the typing rules in the obvious way --- by
> giving mutually-recursive judgements for context well-formedness, type
> and term well-formedness, and equality --- then the definition of the
> type system is clearly structural. However, you will not be able to do
> induction on derivations to prove that weakening is sound, which in
> turn prevents you from being able to show the soundness of
> substitution in any easy way.


What exactly do you mean by "weakening is sound"? As I recall there is no 
problem in proving weakening by induction on derivations in Martin-Lof type 
theory. 

Vladimir.






On Aug 12, 2014, at 8:28 PM, Neel Krishnaswami 
<krishnan AT cs.bham.ac.uk>
 wrote:

> On 11/08/14 11:51, Andrej Bauer wrote:> On Sun, Aug 10, 2014 at 10:25 PM, 
> Abhishek Anand
> > <abhishek.anand.iitg AT gmail.com>
> >  wrote:
> >> The terms (v1:A1 -> B1)  and (v2:A2 -> B2) denote equal PI types in Nuprl
> >> iff
> >> A1 and A2 are equal types
> >> and
> >> forall terms a1 and a2 such that a1 and a2 are equal members of A1,
> >> B1[v1\a1] and B2[v2\a2] are equal types.
> >
> > Unless you intend to introduce crazy recursive types this is not a
> > problem: equality on PI_{x:A} B(x) is defined in terms of equality on
> > A and equality on B, where these two equalities have been previously
> > defined. So this is still a fixpoint which uses structural recursion
> > on the structure of a type. Why would you be unhappy with that?
> 
> If you try to formulate the typing rules in the obvious way --- by
> giving mutually-recursive judgements for context well-formedness, type
> and term well-formedness, and equality --- then the definition of the
> type system is clearly structural. However, you will not be able to do
> induction on derivations to prove that weakening is sound, which in
> turn prevents you from being able to show the soundness of
> substitution in any easy way.
> 
> AFAIK, Nuprl avoids these problems by defining only the universe of
> types and their corresponding PERs recursively, but showing that this
> definition is well-founded requires a surprisingly powerful fixed
> point principle (at least, it surprised me).
> 
> In particular, if you look at Bob Harper's *Constructing Type Systems
> Over an Operational Semantics*, you'll see that he needs the fact that
> a monotone (note: not continuous) function on a CPPO has a least fixed
> point, which is a fixed point principle he establishes by transfinite
> induction and excluded middle. (This is stronger than either the Kleene
> or Knaster-Tarski fixed point theorems.)
> 
> (Martin Escardo and Paul Taylor tell me that Dito Pataraia showed that
> this fixed point theorem also holds in intuitionistic set theory, but
> to my knowledge there isn't a predicative version of it.)
> 
> -- Neel
>

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail