Lambda-abstraction See COMBINATORY LOGIC,. LAMBDA -CALCULU. lambda-calculus, also l-calculus, a theory of mathematical functions that is (a) ‘logic-free,’ i.e. contains no logical constants (formula-connectives or quantifier-expressions), and (b) equational, i.e. ‘%’ is its sole predicate (though its metatheory refers to relations of reducibility between terms). There are two species, untyped and typed, each with various subspecies.
Termhood is always inductively defined (as is being a type-expression, if the calculus is typed). A definition of being a term will contain at least these clauses: take infinitely many variables (of each type if the calculus is typed) to be terms; for any terms t and s (of appropriate type if the calculus is typed), (ts) is a term (of type determined by that of t and s if the calculus is typed); for any term t and a variable u (perhaps meeting certain conditions), (lut) is a term (‘of’ type determined by that of t and u if the calculus is typed). (ts) is an application-term; (lut) is a l-term, the labstraction of t, and its l-prefix binds all free occurrences of u in t. Relative to any assignment a of values (of appropriate type if the calculus is typed) to its free variables, each term denotes a unique entity. Given a term (ts), t denotes a function and (ts) denotes the output of that function when it is applied to the denotatum of s, all relative to a. (lut) denotes relative to a that function which when applied to any entity x (of appropriate type if the calculus is typed) outputs the denotatum of t relative to the variant of a obtained by assigning u to the given x.
Alonzo Church introduced the untyped l-calculus around 1932 as the basis for a foundation for mathematics that took all mathematical objects to be functions. It characterizes a universe of functions, each with that universe as its domain and each yielding values in that universe. It turned out to be almost a notational variant of combinatory logic, first presented by Moses Schonfinkel (1920, written up and published by Behmann in 1924).
Church presented the simplest typed l calculus in 1940. Such a calculus characterizes a domain of objects and functions, each ‘of’ a unique type, so that the type of any given function determines two further types, one being the type of all and only those entities in the domain of that function, the other being the type of all those entities output by that function. In 1972 Jean-Yves Girard presented the first second-order (or polymorphic) typed l-calculus. It uses additional type-expressions themselves constructed by second-order l-abstraction, and also more complicated terms constructed by labstracting with respect to certain type-variables, and by applying such terms to type-expressions. The study of l-calculi has deepened our understanding of constructivity in mathematics. They are of interest in proof theory, in category theory, and in computer science. See also CATEGORY THEORY, COMBINATORY LOGIC , PROOF THEOR. H.T.H.