[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Daniel C. Wang]

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}