User:Ruud Koot/Computer science/Lambda calculus
![]() | This is not a Wikipedia article: This is a workpage, a collection of material and work in progress that may or may not be incorporated into Lambda calculus. It should not necessarily be considered factual or authoritative. |
In mathematical logic and computer science, the lambda calculus (also written as λ-calculus) is a formal system for expressing computation by way of variable binding and substitution.
(pure) untyped lambda calculus (or type-free lambda calculus) (vs. other lambda calculi)
can be interpreted as:
- (inconsistent) proof system (Church vs. types)
- programming language
TODO
[edit]- term vs. expression
- intensionality vs. extensionality
- should we have a separate (techincal) article on the untyped lambda calculus? the proof theoretical properties (normalization, confluence) vary between UTLC, STLC, STLC+fix, STLC+rectypes, Fomega, ...
Outline
[edit]- Lambda calculus: high-level overview of both untyped and typed (some, but not too in-depth metatheory: e.g., model theory for untyped, normalization and a few type systems for typed etc.)
- Untyped lambda calculus: denotation semanatics
- Typed lambda calculus: Normalization theorems, overview of various type systems
History
[edit]- Frege (Begriffschrift, function notation, "currying"), Russel & Whitehead (Principia Mathematica, caret-notation), Gödel's Dialectica interpretation.
- Developed by Alonzo Church in the 1930's as a formal logic (Church 1932) and formalism for defining computable functions (Church 1936, 1941)
- As a formal logic: lambda bindings abstract over universal and existential qunatifiers
- As a formalism for defining computable functions: natural number functions definable in the untyped lambda calculus are the recursive functions (Kleene 1936) and Turing computable functions (Turing 1937)
Syntax
[edit]Abstract syntax
[edit]The abstract syntax of terms (or expressions) M, N, ... in the pure untyped lambda calculus is given in Backus–Naur form (BNF) by:
We assume we have an infinite supply of variables V that the metavariables x, y, z, ... range over.
Concrete syntax
[edit]In the concrete syntax of the lambda calculus the following syntactic conventions are obeyed:
- applications associate to the left;
- the scope of a binder extends to the right as far as possible;
- adjacent binders are merged; and
- superfluous parentheses are omitted.
Example The fully parenthesized term (((λx.(λy.(x y))) M) N) is written as (λxy.x y) M N. The final pair of parentheses cannot be omitted as the then resulting term would correspond to the fully parenthesized term (λx.(λy.(((x y) M) N))) instead.
Free and bound variables
[edit]In an abstraction λx.M the symbol λ is a quantifier or binder that binds all occurrences of the variable x the term M that have not already been bound by a binder inside M. A variable that is not bound is said to be free.
The set of free variables fv(M) occurring in a term M are given by:
Example The free variables fv((λxy.x y z) y) of the term (λxy.x y z) y are {y, z}. Note that it is only the second occurrence of the variable y that is free; the first occurrence is bound.
- Add an image showing the binding structure of a complex expression.
Substitution
[edit]A substitution [P/x]M is a syntactic operation on lambda terms that replaces all free occurrences of the variable x in the term M with the term P:
Failed to parse (unknown function "\begin{array}"): {\displaystyle \begin{array}{rcll} [P/x]x &=& P \\ [P/x]y &=& y &\text{if $x \not\equiv y$} \\ [P/x](M N) &=& ([P/x]M)([P/x]N) \\ [P/x]\lambda x.M &=& \lambda x.M \\ [P/x]\lambda y.M &=& \lambda y.[P/x]M & \text{if $x \not\equiv y$ and $y \notin fv(P)$} \\ [P/x]\lambda y.M &=& \lambda z.[P/x][z/y]M & \text{where $x \notin fv(M) \cup fv(P)$ and $x \not\equiv y,z$} \end{array} }
Example Applying the substitution [λz.z/x] to the term λy.x y (λx.x) gives the term λy.(λz.z) (λx.x). Note that neither the second occurrence of x as a binder, nor the third occurrence of x as a bound variable are substituted for, as they are not free variables.
- capture-avoidance (with some example)
- Due to alpha-renaming, substitutions are deterministic only up to alpha-equivalance.
- Barendregt convention
α-equivalence
[edit]merge this section with Substitutions below?
- syntactic equivalence (≡ and =α)
- de Bruijn indices
Semantics
[edit]Assign meaning to the lambda terms (syntax).
- fairly technical, move after expressiveness?
- (in)consistency
- without types, LC is a system of equalities only
- Church's original (unsound) logic
Proof systems
[edit]Syntactic in nature.
Axiomatic semantics
[edit]An equational proof system.
- substitution (capture-avoiding)
- alpha-renaming, beta-equivalence, symmetry, eta equivalence, transitivity, congruence
Operational semantics
[edit]Reduction rules.
- beta reduction
- properties: confluence, but no termination
- reduction strategies
- redex
- eta-reduction and eta-expansion
Properties
[edit]- normalization
- confluence
Model theory
[edit]Semantic in nature.
Denotational semantics
[edit]- (most naturally stated for typed lambda calculi, considering the untyped as a special instance of such...)
Categorical semantics
[edit]- (only) make sense in a typed setting
Expressiveness
[edit]- probably need to introduce Church numerals before Turing completeness, so we can define lambda-definability of natural number functions
Turing completness
[edit]Church encodings
[edit]Extensions and variations
[edit]Syntax extensions
[edit]- let
- syntactic sugar for application in PULC
- treated differently in HM
- fix (term)
- not needed in PULC
- needed in STLC
Base types
[edit]- booleans, integers
- pairs
- uncurry (curry g) = g (needs surjective pairing and eta-reduction)
- sums
- fix (type)
Typed lambda calculi
[edit]- simply typed: strong normalization/termination; fix
- lambda cube
- Curry-Howard
Combinatory logic
[edit]Applications
[edit]Philosophy
[edit]- Church-Turing thesis
Mathematics
[edit]- foundations
- Entscheidungsproblem
Computer science
[edit]- Landin, programming language theory
- functional programming
Linguistics
[edit]See also
[edit](Topics that probably need to be mentioned or incorporated somewhere in the running text.)
- Currying
- Abstract machines (in particular SECD; add a section on implementation issues?)
Further reading
[edit]Primary / historical
[edit]- Alonzo Church (1932). "A set of postulates for the foundation of logic". Annals of Mathematics, 33(2):346-366.
- Alonzo Church (1933). "A set of postulates for the foundation of logic (second paper)". Annals of Mathematics, 34(4):839-864.
- Alonzo Church (1935). "A proof of freedom from contradiction". Proceedings of the National Academy of Sciences of the United States of America, 21(5):275-281
- Stephen Cole Kleene and J. Barkley Rosser (1935). "The inconsistency of certain formal logics". Annals of Mathematics, 36:630-636.
- Alonzo Church (1936). "A note on the Entscheidungsproblem". Journal of Symbolic Logic, 1(1):40-41
- Alonzo Church (1936). "Correction to A note on the Entscheidungsproblem". Journal of Symbolic Logic, 1(3):101-102
- Alonzo Church (1936). "An unsolvable problem of elementary number theory". American Journal of Mathematics, 58:345-363.
- Stephen Cole Kleen (1936). "Lambda definability and recursiveness". Duke Mathematical Journal, 2:340-353.
- Alan M. Turing (1937). "On computable numbers with an application to the Entscheidungsproblem". Proceedings of the London Mathematical Society, 42:(2):230-265
- Alan M. Turing (1937). "Computability and lambda definability". Journal of Symbolic Logic, 2:153-163.
- Alonzo Church (1940). "A formulation of the simple theory of types". Journal of Symbolic Logic, 5:56-68.
- Alonzo Church (1941). The Calculi of Lambda Conversion. Princeton University Press. (Republished in the Annals of Mathematics Studies, no. 6, 1985)
- Leon Henkin (1950). "Completeness in the theory of types". Journal of Symbolic Logic, 15(2):81-91.
- Haskell B. Curry and Robert Feys (1958). Combinatory Logic I.
Secondary / contemporary
[edit]- Henk P. Barendregt (1984). The Lambda Calculus: Its Syntax and Semantics.
- Henk P. Barendregt (1993). "Lambda calculi with types", in Samson Abramsky, Dov M. Gabbay and Tom Maibaum (eds.), Handbook of Logic in Computer Science, Volume 2, New York: Oxford University Press, pp. 117–309.
- John C. Mitchell (1996). Foundations for Programming Languages. Foundations of Computing. MIT Press. ISBN 0262133210.
- J. Roger Hindley and Jonathan P. Seldin (2008). Lambda-Calculus and Combinators: An Introduction. 2nd edition. Cambridge University Press. ISBN 9780521898850.
- Henk Barendregt, Wil Dekkers, Richard Statman (2010). Lambda Calculus with Types. Cambridge Universty Press. ISBN 9780521766142.
Tertiary
[edit]- Stephen C. Kleene (1981). "Origins of Recursive Function Theory". Annals of the History of Computing 3(1):52-67
- J. Barkley Rosser (1984). "Highlights of the History of the Lambda-Calculus". Annals of the History of Computing 6(4):337-349
- Henk P. Barendregt (1997). "The Impact of the Lambda Calculus in Logic and Computer Science". The Bulletin of Symbolic Logic, 3(2):181–215.
- Felice Cardone and J. Roger Hindley (2009). "Lambda-Calculus and Combinators in the 20th Century" in Dov M. Gabbay and John Woods (eds.), Handbook of the History of Logic, Volume 5: Logic from Russell to Church, Elsevier, pp. 723-817.
- Jonathan P. Seldin (2009). "The Logic of Church and Curry" in Dov M. Gabbay and John Woods (eds.), Handbook of the History of Logic, Volume 5: Logic from Russell to Church, Elsevier, pp. 819-873.
External links
[edit]- "The Lambda Calculus" entry by Jesse Alama in the Stanford Encyclopedia of Philosophy, 8 February 2013
- Shane Steinert-Threlkeld (3 June 2011). "Lambda Calculi". Internet Encyclopedia of Philosophy.
- Lambda calculus entry by David Charles McCarthy}} in the Routledge Encyclopedia of Philosophy, 1998
- "Lambda-calculus", Encyclopedia of Mathematics, EMS Press, 2001 [1994]