[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Frank Pfenning]

Hi Aaron,

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

There is no contest.  The proof theoretic strength alone that is
required to carry out the normalization proof for Coq is much, much
higher than LF.  It took the genius of Girard to develop the method of
"candidats" to give the first normalization proof for the polymorphic
lambda-calculus; normalization for LF is of the same complexity as the
simply typed lambda calculus (extensionality or not).

There is now a presentation of canonical LF using what we call
"hereditary substitutions" which are defined as a simple primitive
recursive functionals (first on the structure of types, then the
structure of terms).  Decidability of this system is immediate and
syntactic.  As yet, there is no presentation for only LF itself, but LF
is a fragment contained in the two papers below if you are curious about
the technique.

But, to re-emphasize, even without this more recent development, LF is
easy and tiny compared to the Calculus of Inductive Constructions.  It
can be so because it is designed only as a logical framework, rather
than a language for (constructive) mathematics.

  - Frank

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A
concurrent logical framework I: Judgments and properties. Technical
Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon
University, 2002. Revised May 2003.
http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf

Contextual Modal Type Theory
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka.
Submitted, September 2005.
http://www.cs.cmu.edu/~fp/papers/cmtt05.pdf

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