Also found in: Dictionary.
Related to lambda-calculus: Untyped lambda calculus


(Normally written with a Greek letter lambda). A branch of mathematical logic developed by Alonzo Church in the late 1930s and early 1940s, dealing with the application of functions to their arguments. The pure lambda-calculus contains no constants - neither numbers nor mathematical functions such as plus - and is untyped. It consists only of lambda abstractions (functions), variables and applications of one function to another. All entities must therefore be represented as functions. For example, the natural number N can be represented as the function which applies its first argument to its second N times (Church integer N).

Church invented lambda-calculus in order to set up a foundational project restricting mathematics to quantities with "effective procedures". Unfortunately, the resulting system admits Russell's paradox in a particularly nasty way; Church couldn't see any way to get rid of it, and gave the project up.

Most functional programming languages are equivalent to lambda-calculus extended with constants and types. Lisp uses a variant of lambda notation for defining functions but only its purely functional subset is really equivalent to lambda-calculus.

See reduction.
This article is provided by FOLDOC - Free Online Dictionary of Computing (
References in periodicals archive ?
The lambda-calculus defines a class of higher-order and partial recursive functions.
In the course of the paper, we have presented syntactic translations from two Algol-like languages into a polymorphic, linear lambda-calculus, given a semantic model of the linear language, and used it characterize the cpo structure of a number of low-order types.
It may have seemed odd that we did use the strict function model, since it is actually a model of relevant lambda-calculus (it models Contraction).
Indeed, linear communications exhibit a partial confluence property reminiscent of the Church-Rosser property of the lambda-calculus, as we show in Section 4.4.
This possibility of partial deadlock or divergence in the pi-calculus gives linear typing a slightly different force than in lambda-calculus, where every linear value will be used unless the whole program fails to yield any result.
For example, to form a pair of two values v and w under some type environment [Gamma] in a linear lambda-calculus, we do not simply check that v and w are well typed in [Gamma]
At this point in compilation, the intermediate code is essentially in a lambda-calculus syntax for assembly language (following the ideas of Wand [1992]).
Call-by-name, call-by-value and the lambda-calculus. TCS 1, 2, 125-159.
As will be demonstrated later, the lambda-calculus and typical concurrent objects can be encoded by using only reliable channels.
Towards a lambda-calculus for concurrent and communicating systems.