Access to the full content is only available to members of institutions that have purchased access. If you belong to such an institution, please log in or find out more about how to order.



Lambda calculus

DOI: 10.4324/9780415249126-Y010-1
Version: v1,  Published online: 1998
Retrieved March 22, 2019, from

Article Summary

The lambda calculus presents a delimited formal setting for expressing and studying properties of mathematical operations and computer programs. Its syntactical unit is the term. Application terms tu represent supplying argument u to routine t. Abstraction terms λx. t (in which λx binds x in t) represent the explicit definition of an operation from a routine t. Term computation is by reduction: (λx. t) (u) reduces to t[x/u], the result of substituting u for x in t; this corresponds to operating with t on u. Terms are equal either when they differ only in bound variables or when one converts to the other via a finite chain of reductions and counter-reductions. There are two main varieties of lambda calculi: typed and untyped (or type-free). Any untyped term is applicable to any other and equality between such terms is undecidable. In the typed case, terms are indexed by types and application is permitted only when types conform. Here, equality is decidable. A. Church proposed formalisms for both varieties during the 1930s. He and his students S. Kleene and J. Rosser proved the early syntactical metatheorems linking the untyped calculus with computability theory. In 1969, D. Scott gave the first set-theoretic construction of a functional model of the untyped calculus; since then, many other models have been devised. As for the typed calculus, Gödel’s Dialectica interpretation inspired many of its applications to proof theory. Also, the idea, due to H. Curry and W. Howard, of using logical formulas as types reveals a close correspondence between typed terms and derivations in intuitionistic formal systems. In the last decades of the twentieth century, the lambda calculus and its models have been put to many uses in computer science, with functional programming and denotational semantics deserving special mention.

Citing this article:
McCarty, David Charles. Lambda calculus, 1998, doi:10.4324/9780415249126-Y010-1. Routledge Encyclopedia of Philosophy, Taylor and Francis,
Copyright © 1998-2019 Routledge.

Related Searches