[POPLmark] Re: adequacy

[Geoffrey A. Washburn]

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