User:Ruud Koot/Computer science/Lambda calculus

See also: User:Wgunther/Lambda Calculus

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:

1. (inconsistent) proof system (Church vs. types)
2. programming language

TODO

• 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

• 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

• 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
    • A paradox was found in the untyped system (Kleene & Rosser 1935) which led to the development of typed variants (Church 1940; Henkin 1950)
  • 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)
    • In the 1960's connections with programming languages were found (Landin 1963, 1965, 1966; Böhm 1966; Strachey 1966; Milne & Strachey 1976; Stoy 1977)

Syntax

Abstract syntax

The abstract syntax of terms (or expressions) M, N, ... in the pure untyped lambda calculus is given in Backus–Naur form (BNF) by:

${\begin{array}{lcll}M,N,...&::=&x&{\text{(variable)}}\\&|&M\ N&{\text{(application)}}\\&|&\lambda x.M&{\text{(abstraction)}}\end{array}}$

We assume we have an infinite supply of variables V that the metavariables x, y, z, ... range over.

Concrete syntax

In the concrete syntax of the lambda calculus the following syntactic conventions are obeyed:

1. applications associate to the left;
2. the scope of a binder extends to the right as far as possible;
3. adjacent binders are merged; and
4. 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

Main article: Free and bound variables

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:

${\begin{array}{lcl}fv(x)&=&\left\{x\right\}\\fv(M\ N)&=&fv(M)\cup fv(N)\\fv(\lambda x.M)&=&fv(M)\backslash \left\{x\right\}\end{array}}$

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

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

merge this section with Substitutions below?

• syntactic equivalence (≡ and =_α)
• de Bruijn indices

Semantics

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

Syntactic in nature.

Axiomatic semantics

An equational proof system.

• substitution (capture-avoiding)
• alpha-renaming, beta-equivalence, symmetry, eta equivalence, transitivity, congruence

Operational semantics

Reduction rules.

• beta reduction
• properties: confluence, but no termination
• reduction strategies
  • redex
• eta-reduction and eta-expansion

Properties

• normalization
• confluence

Model theory

Semantic in nature.

Denotational semantics

• (most naturally stated for typed lambda calculi, considering the untyped as a special instance of such...)

Categorical semantics

• (only) make sense in a typed setting

Expressiveness

• probably need to introduce Church numerals before Turing completeness, so we can define lambda-definability of natural number functions

Extensions and variations

Syntax extensions

• let
  • syntactic sugar for application in PULC
  • treated differently in HM
• fix (term)
  • not needed in PULC
  • needed in STLC

Base types

• booleans, integers
• pairs
  • uncurry (curry g) = g (needs surjective pairing and eta-reduction)
• sums
• fix (type)

Typed lambda calculi

• simply typed: strong normalization/termination; fix
  • lambda cube
  • Curry-Howard

Applications

Philosophy

• Church-Turing thesis

Mathematics

• foundations
• Entscheidungsproblem

Computer science

• Landin, programming language theory
• functional programming

See also

(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

Primary / historical

• 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

• 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

• 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

• "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]