[POPLmark] Re: adequacy

[Geoffrey A. Washburn]

On Mon, 9 May 2005, Geoffrey A. Washburn wrote:

> On Mon, 9 May 2005, Robert Harper wrote:
>
> > It is part of the statement of adequacy for an encoding to specify
> > precisely what is meant by substitution / compositionality.  In the
> > example below you are being mislead by the terminology.  The "leftist
> > substitution" mentioned below would not be the substitution represented
> > as such by the encoding.  Just because something is called substitution
> > doesn't make it so!  BTW, there is no difficulty at all in formalizing
> > lambda-circle in LF.
>
> 	If there is no difficulty I would appreciate it if I could see how
>   you would do so.  Thanks!

	I should also point out that I was not talking about
  lambda-circle; that is, not the circle modality described in Davies'
  paper "A Temporal Logic Approach to Binding Time Analysis" nor the
  circle modality that coincides with the lax modality.  Both of these
  appear to use "standard" notions of substitution.

	I should also point out that you did not address the
  general question of how to reconcile HOAS with notions of substitution
  that are incompatible with substitution in the meta-language.

-- 
-- Geoff Washburn | geoffw at cis.upenn.edu | http://www.cis.upenn.edu/~geoffw/ --