Arithmetic in Lambda Calculus


	Lambda calculus was developed by Alonzo Church and Stephen Kleene in 1930 and consists of a single transformation rule (variable substitution) and a single function definition scheme. It is a system capable of universal computation, that is, any computable function that can be computed in any of the standard programming languages can also be done in lambda calculus, though it might be very hard to actually carry out. Only the basic arithmetic operations successor, testing for zero, addition, multiplication, and exponentiation are considered here. The second numeral is not used for successor or testing for zero.


	Contributed by: Enrique Zeleny Based on programs by: John W. Gray
	Show Initialization Code

The central concept in λ calculus is the "expression". A "name" (or "variable") is an identifier that can be any letter.

An expression is defined recursively as follows:

<function> :=

In order to apply a function to an argument by substituting the argument for a variable in the body of the function and for giving a name to the function determined by a rule, it is necessary to define the following terms:

1) The identity function: ((

) expr) ⇒ expr. If this is applied to any expression, the result is the expression itself.

2) Self-application:

. Applying this to any expression expr results in (expr expr), which may or may not make sense.

3) The Church numerals. The

Church numeral is the lambda expression

, where there are

nested applications of

Some basic definitions are needed for logical testing:

true =

false =

if =

;

and to perform operations:

successor =

is zero? =

addition =

multiplication =

, and

exponentiation =

For further details about the complete description of the operational semantics of the lambda calculus, see J. W. Gray, Mastering Mathematica: Programming Methods and Applications, 2nd ed., San Diego, CA: Academic Press, 1997.