[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Daniel C. Wang]

Karl Crary wrote:
> 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.
>
Are you claiming the on-paper system has no formal meaning? To me the 
adequacy theorem relates two 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?
http://www.cs.cmu.edu/~drl/pubs/hl06mechanizing/hl06mechanizing.pdf
Rule  ENC_TM_VAR in Figure 9. I'm not sure how to interpret it's 
meaning. If both systems were using a nameless, encoding I suspect the 
statement is that the debrujin indexes are the same. I don't think, I 
fully understand the treatment of alpha equivalence for both the 
object-term and the LF term and how you relate them.
> 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).
I don't think, I understand your claim. If I just represent my 
object-logic in Coq as a first-order inductive structure why do I need 
a  normalization result for CIC? I mean a normalization result is needed 
to establish soundness of Coq. But I don't see why it gets dragged in 
for adequacy. Can you construct a very simple example for something like 
the theory of zero, successor, and addition?
> 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!) 
I'll have to admit I don't fully grasp your point. For me the key issue 
is the correspondence between the first-order and higher-order encoding 
because that is where the "controversy" is. i.e. I have an intuitive 
understanding of what first-order syntax "means". I know how to 
represent a theory of first-order syntax formally in many different 
systems, Coq, HOL, ... etc and I understand to some degree what those 
first-order representations "mean". What I and many other people don't 
fully understand is how the higher-order encoding precisely  capture  my 
first-order intuitions in a extremely concise way.