Of historical significance, and still influential. By Nicolaas de Bruijn, from *Indagationes Mathematicae (*1972), available here.

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 [lambda] instead of a name attached to that [lambda]. 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.

### Like this:

Like Loading...

*Related*

see here for the best St Louis roofing available