[POPLmark] Adequacy for LF

[Karl Crary]

Derivations have a notion of free variable, just as syntax does, either 
explicitly or implicitly through hypotheses.  The free variables of a 
derivation induce a notion of substitution on derivations, and that 
should commute with the encoding in the appropriate way.

Note however, that in the case of sub, the question is largely 
degenerate, since you cannot legally substitute for an assumption in an 
algorithmic subtyping derivation, except using another assumption.  To 
see this in the object language, observe that the algorithm treats 
variables specially, so we cannot substitute arbitrary types for them.  
To see it in the encoding (where I think it's actually more clear), 
observe that we have different judgements for assumptions (ie, assm) and 
conclusions (ie, sub).  You can't apply a function expecting an assm to 
a sub.

But a little bit of substitution structure does remain, that of 
subsituting outer assumptions for inner ones, and that should commute 
with the encoding.

    -- Karl



Randy Pollack wrote:

>Karl Crary writes:
> > 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.
>
>What does "respects substitution" mean for the representation of
>derivations of "sub" in file 1a.elf?
>
>Randy
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>