[POPLmark] Adequacy for LF

[Kevin Watkins]

On 5/3/05, Karl Crary <crary at cs.cmu.edu> wrote:
> 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.

Indeed unique decomposition is not required.  Let's adopt the
bijective, compositional representation of evaluation contexts
mentioned in Frank's message (which is one way of viewing what the
Ashley-Rollman solution does).  Although the decomposition can't be
seen directly in the non-normal term being evaluated, it *can* be seen
in the structure of the derivation of (step T T').  The inverse
representation function (mapping LF terms to paper derivations) can
read off the evaluation context from the structure of the derivation. 
This is a key advantage of the LF methodology, where derivations are
reified explicitly as objects.

For those who may not have seen Frank's message, here is the
representation function for evaluation contexts:

  rep([]) = ([x] x) : step T T' -> step T T'.

  rep(E t) = ([x] step_app_fun (rep(E) x))
    : step T T' -> step (T rep(t)) (T' rep(t)).

  rep(v E) = ([x] step_app_arg (rep(E) x) D)
    : step T T' -> step (rep(v) T) (rep(v) T') .
    where D is the derivation establishing that v is a value

  rep(E [T]) = ([x] step_tapp_fun (rep(E) x))
    : step T T' -> step (T rep([T])) (T' (rep([T]))).

The inverse representation function maps a canonical LF term of type
(step T T') into a pair of a paper evaluation context and a primitive
paper evaluation rule (that is, E-APP-ABS or E-TAPP-TABS) in the
obvious way.  We need a simple induction to show that each direction
of the representation works, but that's unavoidable; any adequacy
theorem would need such an induction.

Kevin