Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-23T13:58:50.347Z Has data issue: false hasContentIssue false

A lambda calculus with naive substitution

Published online by Cambridge University Press:  09 April 2009

John Staples
Affiliation:
Department of Mathematics and Computer Science Queensland Institute of TechnologyG.P.O. Box 2434 Brisbane 4001, Australia
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

An alternative approach is proposed to the basic definitions of the lassical lambda calculus. A proof is sketched of the equivalence of the approach with the classical case. The new formulation simplifies some aspects of the syntactic theory of the lambda calculus. In particular it provides a justification for omitting in syntactic theory discussion of changes of bound variable.

Type
Research Article
Copyright
Copyright © Australian Mathematical Society 1979

References

de Bruijn, N. G. (1972), ‘Lambda calculus notation with nameless dummies’, Indag. Math. 34, 381392.CrossRefGoogle Scholar
Hindley, J. R., Lercher, B. and Seldin, J. P. (1972), Introduction to combinatory logic (London Math. Soc. Lecture Notes no. 7, C.U.P., London).Google Scholar
O'Donnell, M. J. (1976), Reduction strategies in subtree replacement systems (Ph.D. Thesis, Cornell University).Google Scholar
Rosen, Barry K. (1973), ‘Tree-manipulating systems and Church-Rosser theorems’, J.A.C.M 20, 160187.Google Scholar
Staples, John (1979), ‘A graph-like lambda calculus for which leftmost-outermost reduction is optimal’, Proceedings of 1978 International Graph Grammars Workshop, Bad Honnef, Germany (Lecture Notes in Computer Science 73, Springer-Verlag, Berlin).Google Scholar