Lambda calculus

Template:Short description

In mathematical logic, the lambda calculus (also written as λ-calculus) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic of this article, is a universal machine, a model of computation that can be used to simulate any Turing machine (and vice versa). It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics. In 1936, Church found a formulation which was logically consistent, and documented it in 1940.

Lambda calculus consists of constructing lambda terms and performing reduction operations on them. A term is defined as any valid lambda calculus expression. In the simplest form of lambda calculus, terms are built using only the following rules:Template:Efn

<math display="inline">x</math>: A variable is a character or string representing a parameter.
<math display="inline">(\lambda x.M)</math>: A lambda abstraction is a function definition, taking as input the bound variable <math>x</math> (between the λ and the punctum/dot .) and returning the body <math display="inline">M</math>.
<math display="inline">(M\ N)</math>: An application, applying a function <math display="inline">M</math> to an argument <math display="inline">N</math>. Both <math display="inline">M</math> and <math display="inline">N</math> are lambda terms.

The reduction operations include:

<math display="inline">(\lambda x.M[x])\rightarrow(\lambda y.M[y])</math> : α-conversion, renaming the bound variables in the expression. Used to avoid name collisions.
<math display="inline">((\lambda x.M)\ N)\rightarrow (M[x:=N])</math> : β-reduction,Template:Efn replacing the bound variables with the argument expression in the body of the abstraction.

If De Bruijn indexing is used, then α-conversion is no longer required as there will be no name collisions. If repeated application of the reduction steps eventually terminates, then by the Church–Rosser theorem it will produce a β-normal form.

Variable names are not needed if using a universal lambda function, such as Iota and Jot, which can create any function behavior by calling it on itself in various combinations.

Explanation and applicationsEdit

Lambda calculus is Turing complete, that is, it is a universal model of computation that can be used to simulate any Turing machine.<ref>Template:Cite journal</ref> Its namesake, the Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote binding a variable in a function.

Template:Anchor Template:AnchorLambda calculus may be untyped or typed. In typed lambda calculus, functions can be applied only if they are capable of accepting the given input's "type" of data. Typed lambda calculi are strictly weaker than the untyped lambda calculus, which is the primary subject of this article, in the sense that typed lambda calculi can express less than the untyped calculus can. On the other hand, typed lambda calculi allow more things to be proven. For example, in simply typed lambda calculus, it is a theorem that every evaluation strategy terminates for every simply typed lambda-term, whereas evaluation of untyped lambda-terms need not terminate (see below). One reason there are many different typed lambda calculi has been the desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus.

Lambda calculus has applications in many different areas in mathematics, philosophy,<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref> linguistics,<ref>Template:Cite book</ref><ref>Template:Cite book</ref> and computer science.<ref>Template:Cite book.</ref><ref>Template:Cite tech report</ref> Lambda calculus has played an important role in the development of the theory of programming languages. Functional programming languages implement lambda calculus. Lambda calculus is also a current research topic in category theory.<ref>Template:Cite book</ref>

HistoryEdit

Lambda calculus was introduced by mathematician Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.<ref>Template:Cite journal</ref>Template:Efn The original system was shown to be logically inconsistent in 1935 when Stephen Kleene and J. B. Rosser developed the Kleene–Rosser paradox.<ref>Template:Cite journal</ref><ref>Template:Cite journal</ref>

Subsequently, in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped lambda calculus.<ref name="Church1936">Template:Cite journal</ref> In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus.<ref>Template:Cite journal</ref>

Until the 1960s when its relation to programming languages was clarified, the lambda calculus was only a formalism. Thanks to Richard Montague and other linguists' applications in the semantics of natural language, the lambda calculus has begun to enjoy a respectable place in both linguistics<ref name='mm-linguistics'>Template:Cite book</ref> and computer science.<ref>{{#invoke:citation/CS1|citation |CitationClass=web }}</ref>

Origin of the λ symbolEdit

Template:Anchor There is some uncertainty over the reason for Church's use of the Greek letter lambda (λ) as the notation for function-abstraction in the lambda calculus, perhaps in part due to conflicting explanations by Church himself. According to Cardone and Hindley (2006):

By the way, why did Church choose the notation "λ"? In [an unpublished 1964 letter to Harald Dickson] he stated clearly that it came from the notation "<math>\hat{x}</math>" used for class-abstraction by Whitehead and Russell, by first modifying "<math>\hat{x}</math>" to "<math>\land x</math>" to distinguish function-abstraction from class-abstraction, and then changing "<math>\land</math>" to "λ" for ease of printing.
This origin was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and λ just happened to be chosen.

Dana Scott has also addressed this question in various public lectures.<ref>Dana Scott, "Looking Backward; Looking Forward", Invited Talk at the Workshop in honour of Dana Scott's 85th birthday and 50 years of domain theory, 7–8 July, FLoC 2018 (talk 7 July 2018). The relevant passage begins at 32:50. (See also this extract of a May 2016 talk at the University of Birmingham, UK.)</ref> Scott recounts that he once posed a question about the origin of the lambda symbol to Church's former student and son-in-law John W. Addison Jr., who then wrote his father-in-law a postcard:

Dear Professor Church,
Russell had the iota operator, Hilbert had the epsilon operator. Why did you choose lambda for your operator?

According to Scott, Church's entire response consisted of returning the postcard with the following annotation: "eeny, meeny, miny, moe".

Informal descriptionEdit

MotivationEdit

Computable functions are a fundamental concept within computer science and mathematics. The lambda calculus provides simple semantics for computation which are useful for formally studying properties of computation. The lambda calculus incorporates two simplifications that make its semantics simple. Template:AnchorThe first simplification is that the lambda calculus treats functions "anonymously"; it does not give them explicit names. For example, the function

<math>\operatorname{square\_sum}(x, y) = x^2 + y^2</math>

can be rewritten in anonymous form as

<math>(x, y) \mapsto x^2 + y^2</math>

(which is read as "a tuple of Template:Mvar and Template:Mvar is mapped to <math display="inline">x^2 + y^2</math>").Template:Efn Similarly, the function

<math>\operatorname{id}(x) = x</math>

can be rewritten in anonymous form as

<math>x \mapsto x</math>

where the input is simply mapped to itself.Template:Efn

The second simplification is that the lambda calculus only uses functions of a single input. An ordinary function that requires two inputs, for instance the <math display="inline">\operatorname{square\_sum}</math> function, can be reworked into an equivalent function that accepts a single input, and as output returns another function, that in turn accepts a single input. For example,

<math>(x, y) \mapsto x^2 + y^2</math>

can be reworked into

<math>x \mapsto (y \mapsto x^2 + y^2)</math>

This method, known as currying, transforms a function that takes multiple arguments into a chain of functions each with a single argument.

Function application of the <math display="inline">\operatorname{square\_sum}</math> function to the arguments (5, 2), yields at once

<math display="inline">((x, y) \mapsto x^2 + y^2)(5, 2)</math>

<math display="inline"> = 29</math>,

whereas evaluation of the curried version requires one more step

<math display="inline">\Bigl(\bigl(x \mapsto (y \mapsto x^2 + y^2)\bigr)(5)\Bigr)(2)</math>

<math display="inline"> = (y \mapsto 5^2 + y^2)(2)</math> // the definition of <math>x</math> has been used with <math>5</math> in the inner expression. This is like β-reduction.

<math display="inline"> = 5^2 + 2^2</math> // the definition of <math>y</math> has been used with <math>2</math>. Again, similar to β-reduction.

to arrive at the same result.

The lambda calculusEdit

The lambda calculus consists of a language of lambda terms, that are defined by a certain formal syntax, and a set of transformation rules for manipulating the lambda terms. These transformation rules can be viewed as an equational theory or as an operational definition.

As described above, having no names, all functions in the lambda calculus are anonymous functions. They only accept one input variable, so currying is used to implement functions of several variables.

Lambda termsEdit

The syntax of the lambda calculus defines some expressions as valid lambda calculus expressions and some as invalid, just as some strings of characters are valid computer programs and some are not. A valid lambda calculus expression is called a "lambda term".

The following three rules give an inductive definition that can be applied to build all syntactically valid lambda terms:Template:Efn

Template:Anchor variable Template:Mvar is itself a valid lambda term.
if Template:Mvar is a lambda term, and Template:Mvar is a variable, then <math>(\lambda x.t)</math>Template:Efn is a lambda term (called an abstraction);
if Template:Mvar and Template:Mvar are lambda terms, then <math>(t s)</math> is a lambda term (called an application).

Nothing else is a lambda term. That is, a lambda term is valid if and only if it can be obtained by repeated application of these three rules. For convenience, some parentheses can be omitted when writing a lambda term. For example, the outermost parentheses are usually not written. See § Notation, below, for an explicit description of which parentheses are optional. It is also common to extend the syntax presented here with additional operations, which allows making sense of terms such as <math>\lambda x.x^2.</math> The focus of this article is the pure lambda calculus without extensions, but lambda terms extended with arithmetic operations are used for explanatory purposes.

Template:Anchor An abstraction <math>\lambda x.t</math> denotes an § anonymous function Template:Efn that takes a single input Template:Mvar and returns Template:Mvar. For example, <math>\lambda x.(x^2+2)</math> is an abstraction representing the function <math>f</math> defined by <math>f(x) = x^2 + 2,</math> using the term <math>x^2+2</math> for Template:Mvar. The name <math>f</math> is superfluous when using abstraction. The syntax <math>(\lambda x.t)</math> binds the variable Template:Mvar in the term Template:Mvar. The definition of a function with an abstraction merely "sets up" the function but does not invoke it.

Template:Anchor An application <math>t s</math> represents the application of a function Template:Mvar to an input Template:Mvar, that is, it represents the act of calling function Template:Mvar on input Template:Mvar to produce <math>t(s)</math>.

A lambda term may refer to a variable that has not been bound, such as the term <math>\lambda x.(x+y)</math> (which represents the function definition <math>f(x) = x + y</math>). In this term, the variable Template:Mvar has not been defined and is considered an unknown. The abstraction <math>\lambda x.(x+y)</math> is a syntactically valid term and represents a function that adds its input to the yet-unknown Template:Mvar.

Parentheses may be used and might be needed to disambiguate terms. For example,

Template:Anchor<math>\lambda x.((\lambda x.x)x)</math> is of form <math>\lambda x.B</math> and is therefore an abstraction, while
<math>(\lambda x.(\lambda x.x)) x</math> is of form <math>M N</math> and is therefore an application.

The examples 1 and 2 denote different terms, differing only in where the parentheses are placed. They have different meanings: example 1 is a function definition, while example 2 is a function application. The lambda variable Template:Mvar is a placeholder in both examples.

Here, example 1 defines a function <math>\lambda x.B</math>, where <math>B</math> is <math>(\lambda x.x)x</math>, an anonymous function <math>(\lambda x.x)</math>, with input <math>x</math>; while example 2, <math>M </math> <math>N</math>, is M applied to N, where <math>M</math> is the lambda term <math>(\lambda x.(\lambda x.x))</math> being applied to the input <math>N</math> which is <math>x</math>. Both examples 1 and 2 would evaluate to the identity function <math>\lambda x.x</math>.

Functions that operate on functionsEdit

In lambda calculus, functions are taken to be 'first class values', so functions may be used as the inputs, or be returned as outputs from other functions.

For example, the lambda term <math>\lambda x.x</math> represents the identity function, <math>x \mapsto x</math>. Further, <math>\lambda x.y</math> represents the constant function <math>x \mapsto y</math>, the function that always returns <math>y</math>, no matter the input. As an example of a function operating on functions, the function composition can be defined as <math>\lambda f. \lambda g. \lambda x. (f ( g x))</math>.

There are several notions of "equivalence" and "reduction" that allow lambda terms to be "reduced" to "equivalent" lambda terms.

Alpha equivalenceEdit

A basic form of equivalence, definable on lambda terms, is alpha equivalence. It captures the intuition that the particular choice of a bound variable, in an abstraction, does not (usually) matter. For instance, <math>\lambda x.x</math> and <math>\lambda y.y</math> are alpha-equivalent lambda terms, and they both represent the same function (the identity function). The terms <math>x</math> and <math>y</math> are not alpha-equivalent, because they are not bound in an abstraction. In many presentations, it is usual to identify alpha-equivalent lambda terms.

The following definitions are necessary in order to be able to define β-reduction:

Free variablesEdit

The free variablesTemplate:Efn of a term are those variables not bound by an abstraction. The set of free variables of an expression is defined inductively:

The free variables of <math>x</math> are just <math>x</math>
The set of free variables of <math>\lambda x.t</math> is the set of free variables of <math>t</math>, but with <math>x</math> removed
The set of free variables of <math>t s</math> is the union of the set of free variables of <math>t</math> and the set of free variables of <math>s</math>.

For example, the lambda term representing the identity <math>\lambda x.x</math> has no free variables, but the function <math>\lambda x. y x</math> has a single free variable, <math>y</math>.

Capture-avoiding substitutionsEdit

Suppose <math>t</math>, <math>s</math> and <math>r</math> are lambda terms, and <math>x</math> and <math>y</math> are variables. The notation <math>t[x := r]</math> indicates substitution of <math>r</math> for <math>x</math> in <math>t</math> in a capture-avoiding manner. This is defined so that:

<math>x[x := r] = r</math> ; with <math>r</math> substituted for <math>x</math>, <math>x</math> becomes <math>r</math>
<math>y[x := r] = y</math> if <math>x \neq y</math> ; with <math>r</math> substituted for <math>x</math>, <math>y</math> (which is not <math>x</math>) remains <math>y</math>
<math>(t s)[x := r] = (t[x := r])(s[x := r])</math> ; substitution distributes to both sides of an application
<math>(\lambda x.t)[x := r] = \lambda x.t</math> ; a variable bound by an abstraction is not subject to substitution; substituting such variable leaves the abstraction unchanged
<math>(\lambda y.t)[x := r] = \lambda y.(t[x := r])</math> if <math>x \neq y</math> and <math>y</math> does not appear among the free variables of <math>r</math> (<math>y</math> is said to be "fresh" for <math>r</math>) ; substituting a variable which is not bound by an abstraction proceeds in the abstraction's body, provided that the abstracted variable <math>y</math> is "fresh" for the substitution term <math>r</math>.

For example, <math>(\lambda x.x)[y := y] = \lambda x.(x[y := y]) = \lambda x.x</math>, and <math>((\lambda x.y)x)[x := y] = ((\lambda x.y)[x := y])(x[x := y]) = (\lambda x.y)y</math>.

The freshness condition (requiring that <math>y</math> is not in the free variables of <math>r</math>) is crucial in order to ensure that substitution does not change the meaning of functions.

For example, a substitution that ignores the freshness condition could lead to errors: <math>(\lambda x.y)[y := x] = \lambda x.(y[y := x]) = \lambda x.x</math>. This erroneous substitution would turn the constant function <math>\lambda x.y</math> into the identity <math>\lambda x.x</math>.

In general, failure to meet the freshness condition can be remedied by alpha-renaming first, with a suitable fresh variable. For example, switching back to our correct notion of substitution, in <math>(\lambda x.y)[y := x]</math> the abstraction can be renamed with a fresh variable <math>z</math>, to obtain <math>(\lambda z.y)[y := x] = \lambda z.(y[y := x]) = \lambda z.x</math>, and the meaning of the function is preserved by substitution.

β-reductionEdit

The β-reduction ruleTemplate:Efn states that an application of the form <math>( \lambda x . t) s</math> reduces to the term <math> t [ x := s]</math>. The notation <math>( \lambda x . t ) s \to t [ x := s ] </math> is used to indicate that <math>( \lambda x .t ) s </math> β-reduces to <math> t [ x := s ] </math>. For example, for every <math>s</math>, <math>( \lambda x . x ) s \to x[ x := s ] = s </math>. This demonstrates that <math> \lambda x . x </math> really is the identity. Similarly, <math>( \lambda x . y ) s \to y [ x := s ] = y </math>, which demonstrates that <math> \lambda x . y </math> is a constant function.

The lambda calculus may be seen as an idealized version of a functional programming language, like Haskell or Standard ML. Under this view,Template:Anchor β-reduction corresponds to a computational step. This step can be repeated by additional β-reductions until there are no more applications left to reduce. In the untyped lambda calculus, as presented here, this reduction process may not terminate. For instance, consider the term <math>\Omega = (\lambda x . xx)( \lambda x . xx )</math>. Here <math>( \lambda x . xx)( \lambda x . xx) \to ( xx )[ x := \lambda x . xx ] = ( x [ x := \lambda x . xx ] )( x [ x := \lambda x . xx ] ) = ( \lambda x . xx)( \lambda x . xx )</math>. That is, the term reduces to itself in a single β-reduction, and therefore the reduction process will never terminate.

Template:AnchorAnother aspect of the untyped lambda calculus is that it does not distinguish between different kinds of data. For instance, it may be desirable to write a function that only operates on numbers. However, in the untyped lambda calculus, there is no way to prevent a function from being applied to truth values, strings, or other non-number objects.

Formal definitionEdit

Template:Further

DefinitionEdit

Lambda expressions are composed of:

variables v₁, v₂, ...;
the abstraction symbols λ (lambda) and . (dot);
parentheses ().

The set of lambda expressions, Template:Math, can be defined inductively:

If x is a variable, then Template:Math
If x is a variable and Template:Math then Template:Math
If Template:Math then Template:Math

Instances of rule 2 are known as abstractions and instances of rule 3 are known as applications.<ref>Template:Cite book (Corrections).</ref> See § reducible expression

This set of rules may be written in Backus–Naur form as: <syntaxhighlight lang="bnf">

<expression>  ::= <abstraction> | <application> | <variable>
<abstraction> ::= λ <variable> . <expression>
<application> ::= ( <expression> <expression> )
<variable>    ::= v1 | v2 | ...

</syntaxhighlight>

NotationEdit

To keep the notation of lambda expressions uncluttered, the following conventions are usually applied:

Outermost parentheses are dropped: M N instead of (M N).
Applications are assumed to be left associative: M N P may be written instead of ((M N) P).<ref name="lambda-bound">{{#invoke:citation/CS1|citation

|CitationClass=web }}</ref>

When all variables are single-letter, the space in applications may be omitted: MNP instead of M N P.<ref>{{#invoke:citation/CS1|citation

|CitationClass=web }}</ref>

The body of an abstraction extends as far right as possible: λx.M N means λx.(M N) and not (λx.M) N.
A sequence of abstractions is contracted: λx.λy.λz.N is abbreviated as λxyz.N.<ref name="Selinger">Template:Citation</ref><ref name="lambda-bound" />

Free and bound variablesEdit

The abstraction operator, λ, is said to bind its variable wherever it occurs in the body of the abstraction. Variables that fall within the scope of an abstraction are said to be bound. In an expression λx.M, the part λx is often called binder, as a hint that the variable x is getting bound by prepending λx to M. All other variables are called free. For example, in the expression λy.x x y, y is a bound variable and x is a free variable. Also a variable is bound by its nearest abstraction. In the following example the single occurrence of x in the expression is bound by the second lambda: λx.y (λx.z x).

The set of free variables of a lambda expression, M, is denoted as FV(M) and is defined by recursion on the structure of the terms, as follows:

Template:Math, where x is a variable.
Template:Anchor Template:Math.Template:Efn
Template:Anchor Template:Math Template:Efn

An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic.

ReductionEdit

The meaning of lambda expressions is defined by how expressions can be reduced.<ref>Template:Cite journal</ref>

There are three kinds of reduction:

α-conversion: changing bound variables;
β-reduction: applying functions to their arguments;
η-conversion: expressing extensionality.

We also speak of the resulting equivalences: two expressions are α-equivalent, if they can be α-converted into the same expression. β-equivalence and η-equivalence are defined similarly.

Template:AnchorThe term redex, short for reducible expression, refers to subterms that can be reduced by one of the reduction rules. For example, (λx.M) N is a β-redex in expressing the substitution of N for x in M. The expression to which a redex reduces is called its reduct; the reduct of (λx.M) N is M[x := N].Template:Efn

If x is not free in M, λx.M x is also an η-redex, with a reduct of M.

α-conversionEdit

α-conversion (alpha-conversion), sometimes known as α-renaming,<ref>Template:Citation</ref> allows bound variable names to be changed. For example, α-conversion of λx.x might yield λy.y. Terms that differ only by α-conversion are called α-equivalent. Frequently, in uses of lambda calculus, α-equivalent terms are considered to be equivalent.

The precise rules for α-conversion are not completely trivial. First, when α-converting an abstraction, the only variable occurrences that are renamed are those that are bound to the same abstraction. For example, an α-conversion of λx.λx.x could result in λy.λx.x, but it could not result in λy.λx.y. The latter has a different meaning from the original. This is analogous to the programming notion of variable shadowing.

Second, α-conversion is not possible if it would result in a variable getting captured by a different abstraction. For example, if we replace x with y in λx.λy.x, we get λy.λy.y, which is not at all the same.

In programming languages with static scope, α-conversion can be used to make name resolution simpler by ensuring that no variable name masks a name in a containing scope (see α-renaming to make name resolution trivial).

In the De Bruijn index notation, any two α-equivalent terms are syntactically identical.

SubstitutionEdit

Substitution, written M[x := N], is the process of replacing all free occurrences of the variable x in the expression M with expression N. Substitution on terms of the lambda calculus is defined by recursion on the structure of terms, as follows (note: x and y are only variables while M and N are any lambda expression):

x[x := N] = N

y[x := N] = y, if x ≠ y

(M₁ M₂)[x := N] = M₁[x := N] M₂[x := N]

(λx.M)[x := N] = λx.M

(λy.M)[x := N] = λy.(M[x := N]), if x ≠ y and y ∉ FV(N) See above for the FV

To substitute into an abstraction, it is sometimes necessary to α-convert the expression. For example, it is not correct for (λx.y)[y := x] to result in λx.x, because the substituted x was supposed to be free but ended up being bound. The correct substitution in this case is λz.x, up to α-equivalence. Substitution is defined uniquely up to α-equivalence. See Capture-avoiding substitutions above.

β-reductionEdit

β-reduction (beta reduction) captures the idea of function application. β-reduction is defined in terms of substitution: the β-reduction of (λx.M) N is M[x := N].Template:Efn

For example, assuming some encoding of 2, 7, ×, we have the following β-reduction: (λn.n × 2) 7 → 7 × 2.

β-reduction can be seen to be the same as the concept of local reducibility in natural deduction, via the Curry–Howard isomorphism.

η-conversionEdit

η-conversion (eta conversion) expresses the idea of extensionality,<ref name= etaReduct >Luke Palmer (29 Dec 2010) Haskell-cafe: What's the motivation for η rules?</ref> which in this context is that two functions are the same if and only if they give the same result for all arguments. η-conversion converts between λx.f x and f whenever x does not appear free in f.

η-reduction changes λx.f x to f, and η-expansion changes f to λx.f x, under the same requirement that x does not appear free in f.

η-conversion can be seen to be the same as the concept of local completeness in natural deduction, via the Curry–Howard isomorphism.

Normal forms and confluenceEdit

Template:Further For the untyped lambda calculus, β-reduction as a rewriting rule is neither strongly normalising nor weakly normalising.

However, it can be shown that β-reduction is confluent when working up to α-conversion (i.e. we consider two normal forms to be equal if it is possible to α-convert one into the other).

Therefore, both strongly normalising terms and weakly normalising terms have a unique normal form. For strongly normalising terms, any reduction strategy is guaranteed to yield the normal form, whereas for weakly normalising terms, some reduction strategies may fail to find it.

Encoding datatypesEdit

Template:Further The basic lambda calculus may be used to model arithmetic, Booleans, data structures, and recursion, as illustrated in the following sub-sections i, ii, iii, and § iv.

Arithmetic in lambda calculusEdit

There are several possible ways to define the natural numbers in lambda calculus, but by far the most common are the Church numerals, which can be defined as follows:

Lambda calculus

Explanation and applicationsEdit

HistoryEdit

Origin of the λ symbolEdit

Informal descriptionEdit

MotivationEdit

The lambda calculusEdit

Lambda termsEdit

Functions that operate on functionsEdit

Alpha equivalenceEdit

Free variablesEdit

Capture-avoiding substitutionsEdit

β-reductionEdit

Formal definitionEdit

DefinitionEdit

NotationEdit

Free and bound variablesEdit

ReductionEdit

α-conversionEdit

SubstitutionEdit

β-reductionEdit

η-conversionEdit

Normal forms and confluenceEdit

Encoding datatypesEdit

Arithmetic in lambda calculusEdit

Logic and predicatesEdit

PairsEdit

Additional programming techniquesEdit

Named constantsEdit

Recursion and fixed pointsEdit

Standard termsEdit

Abstraction eliminationEdit

Typed lambda calculusEdit

Reduction strategiesEdit

ComputabilityEdit

ComplexityEdit

Lambda calculus and programming languagesEdit

Anonymous functionsEdit

Parallelism and concurrencyEdit

SemanticsEdit

Variations and extensionsEdit

See alsoEdit

Further readingEdit

NotesEdit

ReferencesEdit

External linksEdit