[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Karl Crary]

Daniel C. Wang wrote:

> Karl Crary wrote:
>
>> 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.


Of course not.  If you like, read "formal" as "mechanized."  Obviously, 
we cannot have a mechanized proof of a correspondence between an 
on-paper system and a mechanized system.

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


I do not understand your objection.  Are you saying you would prefer to 
use an explicit isomorphism between object language variables and 
meta-language variables, instead of identifying them?  You could do so, 
but I fail to see that would be any more enlightening.  As to the 
second, since we're talking about free variables, I don't see how 
alpha-conversion is an issue.

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


Remember that adequacy goes both ways.  Let's suppose my object language 
judgement is "m + n = o".  Let me write the embedding using brackets.  I 
want to show that there is an isomorphism between derivations of "m + n 
= o" and terms of type "add [m] [n] [o]".  The left-to-right direction 
is easy, but how do you show right-to-left?  You need to consider all 
the terms that could have that type, and they don't have any useful 
structure.  So you need to limit your attention to normal forms, and 
justifying that requires a normalization result.

In case you might imagine that there could be some other, more clever 
way to prove adequacy, consider this:  Our embedding will convert object 
language derivations to normal forms. Therfore, we can normalize terms 
of type "add [m] [n] [o]" by applying the isomorphism in each 
direction.  Therefore, normalization (at that type) is a *corollary* of 
adequacy.  You're not going to be able to prove adequacy without 
tackling normalization.


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

I cannot rebut your claim to have an intutition for one and not the 
other.  However, if we want to speak mathematically, we know that an 
encoding precisely captures an object language exactly when we've proven 
they are isomorphic.  Prove the theorem and the matter is settled.  If 
you cannot prove the theorem, the question is still open.

    -- Karl