[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Aaron Stump]

[ 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.