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?

  • 1
    $\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 Feb 22 '17 at 14:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.