[POPLmark] Adequacy for LF

[Randy Pollack]

Amid a blizzard of messages, this question was not answered:

  What does "respects substitution" mean for the representation of
  derivations of "sub" in file 1a.elf?

Randy
---
Randy Pollack writes:
 > 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