[POPLmark] Re: adequacy

[Karl Crary]

Randy,

If I'm understanding your answer, you seem to be saying that 
substitution is not an essential part of the syntax; rather, it is just 
another judgement that is defined over it.  (Correct me if I 
misunderstand you, because you didn't say so explicitly.)  Consequently, 
you seem to say, there is no requirement to show that the correspondence 
between object terms and their encoding respects substitution.

I admit we're in a fuzzy area here, but I think that the fact that no 
one ever writes down a substitution judgement indicates we all see it as 
part of the syntax.  Certainly I think we can all agree that 
alpha-equivalence is nearly always regarded as an essential part of the 
syntax, so any adequate encoding must respect it.  This is not a problem 
for de Bruijn representations, but it is a problem for explicit variables.

    -- Karl


Randy Pollack wrote:

>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
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>
>  
>