[POPLmark] Poplmark Digest, Vol 10, Issue 5
crary at cs.cmu.edu
Fri Jun 2 11:53:50 EDT 2006
You complain that the theory of adequacy for LF is somehow suspect, and
suggest you'd like to see it formalized. This seems silly to me, for at
least three reasons:
1- The adequacy theorem shows the correspondence between the on-paper
system and the formalized system. It therefore quite obviously cannot
be formalized, as we can only formalize proofs relating formal systems.
2- I believe that the theory of adequacy for LF is entirely solid and
well understood. This is the first time I've ever heard it asserted
that it takes any liberties at all. Can you back up your criticism with
3- LF is the only formalization methodology that even has a developed
theory of adequacy in the first place. Technically speaking, only one
Poplmark solution has been submitted, because only for the Twelf
solution is there an argument that the formalized proof tells you
anything about the original system.
I want to focus on the third point, because I think a lot of people do
not appreciate it. Adequacy states that there is an isomorphism between
the object language (the "on-paper" system) and its formalization. That
is, there is a bijection between the two systems and that bijection
preserves their structure (ie, it commutes with substitution).
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
Now, what could be done is to formalize a correspondence between a
first-order encoding and a higher-order encoding. (I do not think it
would be difficult to do so; perhaps one of the students on the list
will take up the problem.) To do so would in no way be a formalization
of an adequacy theorem, but one could argue that it's the most
interesting part of the adequacy proof. Let's note, however, that
that's a unique property of LF. For Coq, the most interesting part of
the adequacy proof would be the normalization theorem for Inductive
Constructions. (Perhaps we should each get started, and see who
Daniel C. Wang wrote:
>The adequacy theorem you presented in the draft is far from non-trivial.
>I'd personally, would like to see it mechanized in Twelf. The informal
>presentation of the proof in the paper seems to take unfair liberties
>with the treatment of alpha-equality and substitution. In fact every
>adequacy theorem I've seen of this sort seems to take the same liberties.
>It would be nice to see a mechanized treatment of adequacy that shows
>the higher-order encoding is one-to-one with a standard nameless or
>nominal 1st order-encodings. This I understand is a non-trivial request
>but it would be quite ironic if you cannot formalize in Twelf the
>adequacy theorems for which Twelf depends on. It occurs to me that there
>are several ways to state such a theorem in Twelf, some approaches use
>HOAS others are completely first order. I'm not sure which is the most
>interesting one to do.
More information about the Poplmark