[POPLmark] Adequacy for LF

[Karl Crary]

Well, I won't quibble over what is or is not obvious.  To prove it 
rigorously requires two inclusions, one by induction on the evaluation 
context, the other by induction on LF canonical forms.  Both are quite 
simple; quite a bit simpler I think than the other questions considered 
here, but I suppose that's a subjective statement.  Unless I'm very 
confused, no unique decomposition is required.

    -- Karl


Benjamin Pierce wrote:

>>If we agree on this definition, then it is very easy to see that the
>>encoding is adequate.  (Easier than usual, actually.)  Observe that, in the
>>object language, there is exactly one derivation for derivable evaluation
>>judgements.  Similarly, for any E1 and E2, there is at most one canonical
>>form belonging to "step E1 E2".  Thus, the object language and its encoding
>>are in isomorphism provided they agree on the judgement's graph.  We believe
>>the latter is obvious (although to be rigorous would require an inductive
>>proof).
>>    
>>
>
>I think this is where we're really disagreeing.  To me, this "obvious" fact
>is not obvious.  
>
>I believe it's TRUE, of course, but that belief is based on an argument
>(i.e., that the evaluation-context-style and the direct-style operational
>semantics of Fsub are the same relation) that IMHO is of the same order of
>trickiness as the other properties that are being formalized in the
>challenge.  (For example, the proofs of this equivalence that I've seen
>always invoke a "unique decomposition" lemma, saying that any
>non-normal-form t can be factored as t=E[t'] for exactly one E and t'."  The
>proof of this property is not very hard, but it's not trivial either.)
>
>Regards,
>
>    - Benjamin
>
>
>
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>