[POPLmark] Re: adequacy

[Randy Pollack]

Karl Crary writes:
 > 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.

There are many different representations in the class Karl calls FOAS.
For definiteness sake, lets consider Jerome Vouillon's PoplMark
submission using pure de Bruijn representation in Coq.  Jerome's
datatypes "typ" and "term" are concrete descriptions of sets of
well-founded trees.  If you solved the PoplMark challenge informally,
pencil and paper, using pure de Bruijn representation, you would write
some notations intended to denote exactly the same sets of trees.
Each one of these trees is as concrete as a natural number.  So, while
there is still an unavoidable philosophical gap (between "in my mind"
and "on paper"), I don't see any mathematical gap.  Similarly, the
judgements and derivations of Jerome's formalisation are (up to a
philosophical gap) the same sets of concrete trees as an informal
presentation would use.

A different question, genuinely mathematical, is whether pure de
Bruijn representation (either formalised in Coq, or informal pencil
and paper) is an adequate representation of our intended abstract
notion of types or terms with binding.  This question has been
addressed many times, both formally and informally, since de Bruijn's
original paper.  De Bruijn's original paper provides at least as
convincing an adequacy theorem as does LF style adequacy theorems.
Many people (not all) consider that "de Bruijn representation is the
real meaning of lambda terms".

Jerome defines a notion of substitution on these concrete trees, which
corresponds clearly to what de Bruijn wrote in his paper.  Again, the
adequacy of what de Bruijn wrote to represent the informal notion of
substitution has been proven many times.  I don't really see Karl's
point "how do you say that the encoding respects substitution when
FOAS doesn't even have a primitive notion of substitution?"

BTW, the particular meta-logic (Karl asks about Constructions) is
largely irrelevant, as long as we believe it is consistent.  One of
the good things about using LF as a meta-language is that its
consistency is proved in number theory, which is not the case for
Constructions.  But (as a recent contributor asked) what is the logic
of Twelf, and what is the strength of its consistency theorem?  These
seem to be important questions for developing the Twelf approach.

There are many other concrete presentations of lambda terms,
e.g. Curry/Feys, McKinna/Pollack, Gordon/Melham, Stoughton, ...  They
are not all isomorphic.  E.g. neither McKinna/Pollack nor Stoughton's
representation are quotiented by alpha equivalence, but they have
operations that behave well wrt alpha classes. Now things can get
interesting.  We can formally state and prove, in some mechanical
system, relationships between some different representations.
E.g. translations between representations that respect substitution.
One gains confidence in formal definitions by formally relating them
to other formal definitions.  If several formal representations have
(informally proved) adequacy theorems, and we have formally proved
relationships between the representations, that is convincing.

Randy