[TYPES] Strong Normalization for Coq (CiC)

[Eddy Westbrook]

Yes, this is a very fundamental question. This is discussed more in  
the paper, but the basic answer is that I use a "dummy" interpretation  
for proofs, which is essentially like the empty set; i.e., the  
interpretations of proofs  do not "contain" any other terms (where  
"contain" is in a set-theoretic sense). Thus, the interpretation of  
Prop and its types can be built before any of the predicative types.

This may seem counter-intuitive at first, because proofs can contain  
predicative objects. The reason it works, however, is that the only  
way to get predicative objects out of a proof is via an impredicative  
elimination, which must always, in the end, create another proof.  
Thus, such functions always equal  \dummy -> dummy, which we in fact  
eta-contract in the interpretation function to just dummy.

Hope this helps,
-Eddy

On Nov 7, 2011, at 12:54 PM, Sampo Syreeni wrote:

> On 2011-11-03, Eddy Westbrook wrote:
>
>> The basic idea is uniformity, where, instead of defining an  
>> interpretation (aka a logical relation) for only types, or defining  
>> one for types and one for terms, in my approach the interpretation  
>> is defined uniformly on all terms M. When M happens to be a type,  
>> the interpretation is similar to the standard logical relations for  
>> types.
>>
>> The current draft can be found here:
>> http://www.cs.rice.edu/~emw4/uniform-lr.pdf
>
> Will read, but prima facie, how precisely do you avoid the kinds of  
> level problems and self-circularity which lead to type hierarchies  
> in the first place, if you just treat the levels as categorically  
> equivalent? This is an idiot-question, I know, but I also feel it's  
> the first one to be answered in this kind of unifying work.
> -- 
> Sampo Syreeni, aka decoy - decoy at iki.fi, http://decoy.iki.fi/front
> +358-50-5756111, 025E D175 ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2
>