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

@article{citeulike:925759, abstract = {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.}, author = {de Bruijn, N. G.}, citeulike-article-id = {925759}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/1385-7258(72)90034-0}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B7GXJ-4D7KB7T-69/2/f7d94f421509fcef9572e2627bf57e3a}, doi = {10.1016/1385-7258(72)90034-0}, journal = {Indagationes Mathematicae (Proceedings)}, keywords = {debruijn, functionalprogramming}, number = {5}, pages = {381--392}, posted-at = {2008-12-23 06:40:38}, priority = {2}, title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem}, url = {http://dx.doi.org/10.1016/1385-7258(72)90034-0}, volume = {75}, year = {1972} }

TY - JOUR ID - citeulike:925759 L3 - citeulike-article-id:925759 N2 - 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. IS - 5 JF - Indagationes Mathematicae (Proceedings) EP - 392 TI - Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem VL - 75 SP - 381 KW - debruijn KW - functionalprogramming AU - de Bruijn, NG PY - 1972/// UR - http://dx.doi.org/10.1016/1385-7258(72)90034-0 ER -