14
$\begingroup$

A bit of "folklore" in lambda calculus is the idea of characterizing the class of $\beta$-normal terms inductively as a syntactic category ($R$) defined in mutual induction with an auxiliary syntactic category of "neutral" terms ($B$):

$R$ ::= $\lambda x.R \mid B$

$B$ ::= $x \mid B(R)$

This division shows up in many places, such as in bidirectional type checking, normalization-by-evaluation, and in proofs by logical relations. I was recently surprised to see this grammar clearly displayed in an old essay by Don Knuth, "Examples of Formal Semantics" (albeit followed by a word of warning!):

a context-free grammar from p.218 of Knuth (1970)

This is the oldest reference that I know (1970), but Jean-Yves Girard's thesis work was around the same time and also talked explicitly about neutral ("simple") terms in connection with proofs of strong normalization. How far back does the idea go? Did, say, Church or Curry discuss it?

Improve this question
$\endgroup$
1
  • 2
    $\begingroup$ Guess you know that in Proof and Types, pag.41, Girard mentions that it is a contribution of his own: "Some of the technical improvements, such as neutrality, are due to [Gir72]." $\endgroup$
    – Andrea Asperti
    Commented Feb 22, 2017 at 14:35

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.