Lambda calculus
The lambda calculus was invented by Alonzo Church in the 1930s as part of a broader attempt to formalise the foundations of mathematics. That system turned out to be inconsistent, but Church salvaged and published in 19361 just the portion relevant to computation — what is now called the lambda calculus — and this was proved 2 to be consistent that same year.
The lambda calculus is a powerful tool, but tends to frighten away novices because of the word 'calculus' and the seemingly incomprehensible notation. Fortunately, its power and complexity is built on simple rules and intuitions, ones which the average programmer has already been exposed to. Programmers are used to calling functions and sending the values they return to other functions. An example is writing 1 + 2 * 2 as add(1, multiply(2, 2)). The first step in an imperative language would be to replace that code with add(1, 4) after completing the multiply operation. The lambda calculus tries to capture the nested structure of functions within functions. The difference is that functions in imperative languages arrive at a result by executing a series of statements that correspond to an algorithm, whereas we tend to imagine lambda calculus function applications as using a process reminiscent of repeatedly replacing wildcards within a function body. The result is the same: applying a function to its input arguments turns into the value it outputs, and these functions are strung together so that the return value of one becomes the argument of another.
Properties
In lambda calculus a function does not technically 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. Alan Turing3 proved that the set of all functions definable in the lambda calculus is equivalent to the Turing-machine-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 one would naturally or intuitively regard as "effectively computable."
Introduction
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. The intuition is that λ x.E is a function that takes one parameter, x, and returns E. For instance, λ x.x is a function that takes one argument x and immediately returns that argument. A lambda expression is either a variable (like the x in the above expression), a function in the "λ x.E" form, or an application E1E2. Application is jargon for calling a function, and is conventionally written without any brackets. That is, "E1 E2" is an example of calling E1 with E2 as its argument.
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"). Bound variables refer to things within the lambda term, whereas free variables refer to values that aren't already defined within the expression. A pure lambda expression has no free variables — it is self-contained.
Three things can be done with lambda expressions:
- Alpha conversion renames a bound variable: "λ x.x" can be alpha converted to "λ y.y". Variable names are meaningless on their own, so they can be almost freely swapped if all instances of a name are swapped at once.
- 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. Beta reduction is the heart of the lambda calculus; intuitively, it represents transforming a function and its argument into the return value of that function.
- Eta conversion allows us to say that "f" and "λ x.fx" are equivalent. In other words, a function that takes one argument and calls f with it is exactly the same as f itself.
Two shorthand notations are used:
- "λ x1 x2... ...xn.E" means "λ x1. (λ x2. ...(λ xn.E)...)".
- fab means (fa)b.
These shorthand notations make Currying easier, allowing one to pretend these single-argument functions take multiple arguments.
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 nth. 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.