[POPLmark] Re: adequacy

[Robert Harper]

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.

No one is claiming that Twelf is perfect.  But so far no one has come 
up with a meaningful criticism.  The POPLmark challenge draft, for 
example, gives the misleading impression that practically nothing works 
well in the LF methodology, but in fact the opposite is the case --- 
practically everything does!  Much discussion on the mailing list 
misfires as criticism of LF and Twelf, even though we are quite aware 
of shortcomings that have not yet come up on the list.  (In answer to 
Peter's request, I'm waiting until all the spurious discussion dies 
down before raising the more serious issues that came up in our 
solution.)

Bob

On May 9, 2005, at 3:17 PM, Geoffrey A. Washburn wrote:

>
> On Thu, 5 May 2005, Karl Crary wrote:
>
>> So my question is, what is the appropriate notion of adequacy for a 
>> FOAS
>> system such as Constructions?  To me it seems very tricky, because you
>> want to set up an isomorphism between two systems that don't even have
>> the same structure.  That is, how do you say that the encoding 
>> respects
>> substitution when FOAS doesn't even have a primitive notion of
>> substitution?
>>
>> Even in the absence of a rigorous definition, I would be interested to
>> hear how the Coq people think about these matters.
>
> 	I know at least one person who claims to be working with de Bruijn
>   indices in his head when he does paper proofs, so I could imagine he
>   would argue that adequacy would be very straightforward.  I'm not 
> sure I
>   believe that myself, so it would certainly be valuable to hear more 
> on
>   how adequacy theorems are developed for other systems.
>
> 	However, your comment about difficulties with FOAS because it
>   lacks primitive notion of substitution reminds me of an important 
> point
>   about using HOAS a representation technique.  HOAS only works well 
> when
>   the meta-languages notion of substitution coincides with that of the
>   object language.  For example, Pfenning and Davies in their paper "A
>   Judgmental Reconstruction of Modal Logic" define a new form of
>   substitution for the possibility modality
>
> 	<<M / x>> F                  =  [M / x]F
>         <<let dia y = M in E / x>>F  =  let dia y = M in (<<E / x>>F)
>
>   It does not seem possible to provide a straightforward encoding of 
> this
>   kind of substitution via HOAS within LF.  Is there a consensus as 
> how to
>   deal with these sorts of mismatches in substitution other than 
> reverting
>   to FOAS?  The above could admittedly be handled by a hybrid approach,
>   but that might not be true for other notions of substitutions.
>
>        Lest people get the wrong impression, I think Twelf is great
>   technology and quite useful for a number of purposes.  For example, 
> last
>   week I was able to use it to build some theorem provers for modal 
> logics
>   quite quickly.  Still, Twelf is not without its warts.
>
> -- 
> -- 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