# historical question: earliest description of beta-normal terms together with “neutral” terms in lambda calculus?

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!):

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?

• 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]." – Andrea Asperti Feb 22 '17 at 14:35