[POPLmark] Adequacy for LF

[Benjamin Pierce]

> 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