[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Karl Crary]

Of course, I was talking about Coq, not HOL, because I think I have a 
pretty good idea of what you would do in Coq to state adequacy.  I agree 
that in HOL you would probably state it quite differently, but it's not 
as obvious what that might be to me as it seems to be to you.  Perhaps 
you could work this out.

However, no matter how you decide to state adequacy, you are still 
ultimately trying to provide an isomorphism between the object language 
and some concept in the meta-language.  That means that you are going to 
need some strategy for dealing with the meta-language's proof theory.  
At the very least you will need consistency, or the meta-language tells 
you nothing at all.

    -- Karl


Daniel C. Wang wrote:
> Here is the disconnect between our understandings.     *terms of type 
> "add [m] [n] [o]".*
> I think you assume a particular representation technique that relies 
> on dependent types. If I were doing this in HOL "add" would just be a 
> relation defined as a fixpoint of some functor. Not an object whose 
> dependent type represents the proposition. I think, I see your point, 
> but that point assumes a particular representation technique for my 
> relation which I'm not forced to use. Does this sound correct?
>
>
> Karl Crary wrote:
> {stuff deleted}
>> 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.
>>   
> {stuff deleted}
>