# Lambda calculus

The **lambda calculus** was invented by Alonzo Church in the 1930s as part of an attempt to construct a formal system for the foundations of mathematics. When that system turned out to be inconsistent, Church isolated and published in 1936^{1} just the portion relevant to computation — what is now called the lambda calculus — and this was proved ^{2} to be consistent that same year.

In lambda calculus a function does not *return* a result based on its parameters — instead the function and its parameters are *reduced* to give an answer, which mathematically is equivalent to the question. Turing^{3} proved that the lambda-definable functions coincide with the Turing-computable functions (so lambda calculus is Turing-complete), thereby lending credence to the thesis — now called the Church-Turing thesis — that it's these functions, and these functions only, that would naturally or intuitively be regarded as "effectively computable."

The following paragraphs give an informal introduction to lambda calculus — for a formal description of lambda calculus see under "External resources."

A function in lambda calculus is written in the form "λ x.E", where x is the function's parameter and E is a lambda expression constituting the function body. A lambda expression is either a variable (like the x in the above expression), a function in the form above, or an application E1E2.

In the expression "λ x.E", any occurrence of x in E is *bound*, while any other variable is *free* (unless bound by another lambda expression, like the y in "λ x.λ y.xy"). A *pure* lambda expression has no free variables.

Three things can be done with lambda expressions:

- Alpha conversion renames a bound variable: "λ x.x" can be alpha converted to "λ y.y".
- Beta reduction allows applications to be reduced: "(λ x.E1)E2" can be beta reduced to E1 with all occurrences of x replaced with E2. If there are name clashes (for example in "(λ x.λ y.xy)y"), alpha conversion may be required first.
- Eta conversion allows us to say that "f" and "λ x.fx" are equivalent.

Two shorthand notations are used:

- "λ x1 x2... ...xn.E" means "λ x1. (λ x2. ...(λ xn.E)...)"
- fab means (fa)b

## Examples

It may not be initially clear how lambda calculus can carry out any useful computation. In this section of the document the basics of integer arithmetic in lambda calculus are shown — see under "External resources" for further examples of recursion, boolean logic and the representation of tuples and lists.

The most common representation of integers in lambda calculus is the idea of Church numerals, where *n* is represented by the concept *n*th. In particular:

- zero = λ fx.x
- one = λ fx.fx
- two = λ fx.f(fx)
- three = λ fx.f(f(fx))

Where the function *f* is applied *n* times. We can now represent the concept of increment by the lambda expression:

λ nfx.f(nfx)

To see how this works, we can apply it to the Church numeral for two:

(λ nfx.f(nfx))(λ fx.f(fx))

By alpha conversion and beta reduction this becomes:

λ fx.f((λ gy.g(gy))fx)

Which by further beta reduction becomes:

λ fx.f(f(fx))

Which we can see is the Church numeral for three.

## References

- A. Church, "An unsolvable problem of elementary number theory",
*American Journal of Mathematics*, Volume 58 (1936), pp. 354-363. - A. Church and J. B. Rosser, "Some properties of conversion",
*Transactions of the American Mathematical Society*, Volume 39 (1936), pp. 472-482. - A. Turing, "Computability and lambda definability",
*Journal of Symbolic Logic*, Volume 2 (1937), pp. 153-163. - H. Barendregt, "The Impact of the Lambda Calculus in Logic and Computer Science",
*The Bulletin of Symbolic Logic*, Volume 3, Number 2, June 1997.

## See also

## External resources

- Lambda calculus at Wikipedia
- Lambda Calculus (at Safalra's Website)
- Formal Description Of Lambda Calculus
- Alligator eggs introduces a representation of lambda calculus terms by families of crocodiles. Lambda abstractions and variables are represented by hungry colored crocodiles and colored eggs. Each variable name corresponds to a color. If you lambda-abstract an expression, then the hungry crocodile is guarding that expression, which is represented by the expression drawn below the colored crocodile. Hungry crocodiles face right, and application is represented by the two expressions next to each other, so that when an argument is applied to a lambda expression, the hungry crocodile can eat the argument. Parenthesized expressions are represented by an old (colorless) crocodile guarding a family.