[POPLmark] Adequacy for LF

[Karl Crary]

There's been some confusion about the adequacy of our encoding of the 
operational semantics; in particular, why our encoding is adequate, 
given that the paper presents the semantics using evaluation contexts 
and our encoding does not.  We wanted to clarify why it is adequate, and 
moreover, why we thought its adequacy was obvious.

The central point is the definition of adequacy.  Following the original 
paper on LF, we say that an encoding is adequate exactly when it defines 
a bijection between constructs in the object language and canonical 
forms (of appropriate type in an appropriate context) in LF, and that 
bijection respects substitution.

Why is this the right definition?  Since the set of object language 
terms/derivations and the set of LF canonical forms are entirely 
different sets, they can only be meaningfully related by isomorphism.  
And, since the only structure in this setting is substitution, an 
isomorphism is a bijection that respects substitution.  That's all:  To 
claim that an encoding of the operational semantics should "use 
evaluation contexts" is like saying that any group isomorphic to Z_k 
needs to "use addition."  Getting rid of such unimportant presentation 
details is exactly what isomorphisms are all about.

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

    -- Karl and Bob