×

Axioms for the theory of lambda-conversion. (English) Zbl 0587.03008

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.

MSC:

03B40 Combinatory logic and lambda calculus
03-04 Software, source code, etc. for problems pertaining to mathematical logic and foundations

Software:

PL/I
PDFBibTeX XMLCite
Full Text: DOI