[POPLmark] Re: adequacy

[Karl Crary]

First, let me split a nomenclatural hair:  LF is not (just) a type 
system; it is a methodology for expressing deductive systems that 
happens to be based in part on a type system.  The idea of adequacy is 
at least as important to working in LF than the language itself.  If you 
look at the original LF paper, you'll find that most of it is concerned 
with the formalization and proof of adequacy.  I'm happy now to move on 
to focus on the Twelf meta-logic, but a clear understanding of LF is a 
pre-requisite, so I don't begrudge the time we've spent on it.

Now let me indulge in a challenge of my own.  I claim that a precise 
notion of adequacy is a pre-requisite to any formalization of a logic.  
Without it, there's no way to say when you've formalized it correctly or 
not.  LF has such a notion, and it comes out fairly cleanly due to LF's 
use of HOAS.

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.

    -- Karl



Geoffrey A. Washburn wrote:

>On Tue, 3 May 2005, Karl Crary wrote:
>
>	I think maybe one point that has not been emphasized enough is
>  that many of the difficulties that some people at Penn (and elsewhere)
>  are having trying to understand the Twelf solution are not because
>  they are having trouble understanding LF.  I think everyone here
>  has a handle on the LF type system.  The problem is that in order
>  for a well-typed LF signature to be considered a proof, Twelf must
>  verify a number of properties about the signature (coverage, totality,
>  termination, etc.).  The reasoning used by Twelf internally to determine
>  whether a signature has the necessary properties is not easy to grasp,
>  and to my knowledge there are no approachable resources for the
>  uninitiated that clearly explain the process and common pitfalls.
>
>  
>