Jump to content

User:Ruud Koot/Computer science/Lambda calculus

From Wikipedia, the free encyclopedia

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

[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
      • 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

[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:

  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

[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 yx.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]

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.)

Further reading

[edit]

Primary / historical

[edit]

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]
[edit]