[POPLmark] Re: adequacy

[Karl Crary]

Here's what I would suggest you try:  Add a type of worlds with no 
constants, and a judgement that says that a world is current.  Truth 
assumptions should be relative to a particular world, and should only be 
usable when the world is current.  By withholding the currency of a 
world, you can eliminate the world-specific judgements.

    -- Karl


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!
>
>  
>