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

N.G. Bruijn, de

Research output: Contribution to journalArticleAcademicpeer-review

261 Citations (Scopus)


In ordinary lambda calculus the occurrences of a bound variable are made recognizable by the use of one and the same (otherwise irrelevant) name at all occurrences. This convention is known to cause considerable trouble in cases of substitution. In the present paper a different notational system is developed, where occurrences of variables are indicated by integers giving the "distance" to the binding ¿ instead of a name attached to that ¿. The system is claimed to be efficient for automatic formula manipulation as well as for metalingual discussion. As an example the most essential part of a proof of the Church-Rosser theorem is presented in this namefree calculus.
Original languageEnglish
Pages (from-to)381-392
JournalIndagationes Mathematicae (Proceedings)
Issue number5
Publication statusPublished - 1972


Cite this