[POPLmark] Poplmark Digest, Vol 10, Issue 5

Karl Crary crary at cs.cmu.edu
Mon Jun 5 12:25:00 EDT 2006


Aaron,

I appreciate your comments, but I have to disagree on several points.  
First, the canonization proof for LF you refer to is not at all 
complicated.  Quite the contrary, it is a simple proof based on a good 
idea.  Not every research result is complicated.  On the other hand, 
with no disrespect intended to Benjamin Werner, I cannot imagine that 
anyone would call the normalization proof for CIC simple.

Secondly, and much more importantly, it is incorrect that adequacy 
results in LF depend on canonization.  (Indeed, LF's adequacy 
methodology pre-dates the canonization result by several years.)  
Adequacy in LF expresses an isomorphism between the object language and 
LF *canonical forms.*  We do not need to prove canonization, because we 
limit our attention to canonical forms in the first place.  
(Canonization is important for justifying the way the Elf/Twelf 
*implementation* works, but that is not a matter of adequacy per se!)

For technical reasons, I do not think that the same device can be used 
in Coq.  LF's canonical forms methodology relies crucially on the fact 
that canonical forms are eta-long.  In LF, eta-long forms are closed 
under substitution, but Constructions they are not, due to 
polymorphism.  Moreover, it's not  clear what eta-long would mean in 
Inductive Constructions, due to inductive types.  So I think it is 
accurate to say that while canonization in not crucial to adequacy in 
LF, it probably would be crucial in Coq.

Thirdly, Coq is not CIC.  To my knowledge, normalization for Coq's type 
theory is an open problem.

Finally, even if we restrict our attention to CIC, as far as I know, it 
is still only conjecture to say that CIC embeddings are adequate.  It 
seems that it might be easy to prove (modulo the normalization proof), 
but no one has yet done it.  I would love it if someone from the Coq 
community would do this, if only to give us a solid basis for comparison.

    -- Karl



Aaron Stump wrote:
> [ responding to Karl, see below ]
>
> I appreciate the very clear and helpful way in which you are describing
> the connection between adequacy and normalization.  Coq encodings are
> every bit as adequate as Twelf encodings, however, because CIC does
> enjoy strong normalization.  Indeed, I dispute the point you make below
> that adequacy is obvious for LF and complicated for other systems,
> precisely because (as you probably know better than I) adequacy depends
> on the existence of canonical forms in LF, which is arguably a *deeper*
> result than normalization for CIC.  In my current work I am bumping up
> against the lack of extensionality in Coq, so I have a renewed
> appreciation for extensionality in LF.  Nevertheless, extensionality
> makes LF, in this respect, a stronger type theory than CIC.  It is
> needed for the representation techniques typically used with LF, so it
> is really essential.  A satisfactory account of the meta-theory with
> extensionality (again, as I'm sure you know better than I) proved quite
> difficult and was a significant research accomplishment of your
> colleagues at CMU.  In contrast, the meta-theory of type theories like
> CIC's without extensionality is easier.
>
> So both for Coq and LF, adequacy depends on normalization.  The question
> of which system has an an easier normalization result and hence a
> simpler account of adequacy is at the very least, not as overwhelmingly
> in LF's favor as you claim.
>
> Aaron
>
>   
>> For LF, it is quite easy to prove the adequacy theorem because the 
>> system is weak enough that the type of a term dictates its structure.  
>> The allows us to prove using a simple induction that an object language 
>> derivation exists whenever an LF term of the appropriate type exists.
>>
>> For contrast, let me pick on Coq.  In Coq, a term can have almost any 
>> structure.  This means that adequacy for Coq representations would 
>> depend on a very deep normalization result for the Calculus of Inductive 
>> Constructions.  (As an aside, we can note here that, to my knowledge, 
>> the normalization proof has never been extended to cover some important 
>> axioms in the Coq implementation.)  Still, I think it's easy to imagine 
>> how one would do it (modulo the extra axioms), and I would be very 
>> interested to see someone work this story out.  I think the high-level 
>> story would be similar for HOL + Nominal Logic, except the account of 
>> compositionality would be more complicated (and more interesting).
>>
>> My point here is that you seem to be thinking that adequacy is 
>> complicated for LF and obvious for other systems, where in fact the 
>> exact opposite is true.  This has nothing to do with first-order vs. 
>> higher-order representations; it has to do with the advantages of a weak 
>> type theory.
>>     
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>   


More information about the Poplmark mailing list