[POPLmark] Re: adequacy

[Robert Harper]

I was referring to the lambda circle that codifies the lax modality 
(monad).

There is no general answer.  Dating back to the earliest days of LF, we 
considered many different logics and many different notions of 
substitution and consequence; each presents its own problems and is 
solved in its own manner.  One cannot make blanket statements about the 
applicability or inapplicability of HOAS to representing logics.  You 
can do much more than would be thought possible at a naive first 
reading; it is also true that there are cases that are very hard to 
handle adequately.  For a comprehensive study see Marino Miculan's 
Udine PhD thesis.  Do not expect sweeping generalities, but also do not 
underestimate what can be done.

Bob

On May 9, 2005, at 5:35 PM, Geoffrey A. Washburn wrote:

> 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/ --
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark