[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Karl Crary]

Dan,

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 
some specifics?

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


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 
finishes first!)

    -- Karl



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