Discussing 'Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem'

(Link).

Author: N. G. de Bruijn (Eindhoven University of Technology)

Reference: Indagationes Mathematicae Vol. 75(5), pp 381-392 (1972).

Why this paper? Cited by 4 (of a possible 29) of the papers in my Google Scholar Updates recommendations.

Comments: As the papers I discuss for this blog are those most cited in my Google Scholar 'Updates' recommendations, it is not surprising that the 'classic papers' I've looked at so far have been very closely related to my research interests. This week's paper is slightly further away, but is a classic indeed, notable enough to have a pretty good Wikipedia article about it (Wikipedia's 'nominal techniques' article is, by comparison, a neglected stub).

De Bruijn indices are one solution to the problems of names and binding which we've discussed on this blog before. They work by eradicating names altogether. This is an apparently brutal but very well-motivated idea, because the choice of names, for example of variables in a computer program, is formally arbitrary. So why have them?

There are two main answers to this rhetorical question. The first is that names allow the 'internal book-keeping' needed to keep track of what is being referred to at various points inside a program. De Bruijn's contribution is to show that this style of book-keeping can be replaced by counting how many steps there are between the introduction of (what we'd usually consider) a name, and its use.

The second answer to my rhetorical question is that, as openly admitted by de Bruijn in the introduction, names seem essential for human-readable syntax. De Bruijn frames his alternative approach as a tool for automation, as well as programming, and indeed in these contexts his approach has flourished and remains important. But there is now much interest in formalising human proofs, and in interactive theorem proving in which human and computer work together towards a proof, and so combining human-readability with full formality is an important goal. This is the niche in which nominal techniques (and some approaches as well) have become prominent. In fact even de Bruijn's contribution can be seen in this light, as there does exist another, much older, nameless approach based on so-called 'combinators'; de Bruijn's approach sits much closer to human practice.