Revesz, Gyorgy Axioms for the theory of lambda-conversion. (English) Zbl 0587.03008 SIAM J. Comput. 14, 373-382 (1985). In the standard presentations of \(\lambda\)-calculus the operation of substitution is defined as a primitive operation and used in the definition of convertibility. In the present paper we show that the axioms for the theory of lambda-conversion can be simplified in such a way that substitution is not needed at all, as it is reduced to a more elementary operation of replacement without giving up the intuitive simplicity of the lambda-notation. This is achieved by making essential use of the properties of substitution in formulating the axiom system. Also, another unusual axiom system will be presented which uses renaming that replaces every (free or bound) occurrence of a variable by another. Finally, we give the outline of a program written in PL/I that computes the normal form (if any) of \(\lambda\)-terms by using our axioms. Cited in 1 ReviewCited in 4 Documents MSC: 03B40 Combinatory logic and lambda calculus 03-04 Software, source code, etc. for problems pertaining to mathematical logic and foundations Keywords:lambda calculus; program for computing normal form of lambda-terms; substitution; replacement; renaming Software:PL/I PDFBibTeX XMLCite \textit{G. Revesz}, SIAM J. Comput. 14, 373--382 (1985; Zbl 0587.03008) Full Text: DOI