Editing Lambda calculus (section)

=== The lambda calculus ===
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 terms ====
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:{{efn|name=lamTerms|1= The expression e can be:   variables x, lambda abstractions, or applications —in BNF, <math>e ::= x \mid \lambda x.e \mid e \, e</math> .— ''from Wikipedia's [[Simply typed lambda calculus#Syntax]] for untyped lambda calculus}}
*{{anchor|validLambdaVar}} variable {{mvar|x}} is itself a valid lambda term.
*if {{mvar|t}} is a lambda term, and {{mvar|x}} is a variable, then <math>(\lambda x.t)</math>{{efn| <math>(\lambda x.t)</math> is sometimes written in [[ASCII]] as <math>L x.t</math>}} is a lambda term (called an ''abstraction'');
*if {{mvar|t}} and {{mvar|s}} 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|§ 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.

{{anchor|lambdaAbstr}} An ''abstraction'' <math>\lambda x.t</math> denotes an [[#anonymousForm|§ anonymous function]]{{efn|The lambda term <math>(\lambda x.t)</math> represents the function <math>x \mapsto t</math> written in anonymous form.}} that takes a single input {{mvar|x}} and returns {{mvar|t}}. 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 {{mvar|t}}. The name <math>f</math> is superfluous when using abstraction. The syntax <math>(\lambda x.t)</math> [[Free variables and bound variables|binds]] the variable {{mvar|x}} in the term {{mvar|t}}. The definition of a function with an abstraction merely "sets up" the function but does not invoke it.

{{anchor|anApplic}} An ''application'' <math>t s</math> represents the application of a function {{mvar|t}} to an input {{mvar|s}}, that is, it represents the act of calling function {{mvar|t}} on input {{mvar|s}} 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 {{mvar|y}} 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 {{mvar|y}}.

Parentheses may be used and might be needed to disambiguate terms. For example, 
#{{anchor|Example1parenRightIsAbstraction}}<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 {{mvar|x}} is a placeholder in both examples.

Here, [[#Example1parenRightIsAbstraction|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>&nbsp;<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 functions ====
In lambda calculus, functions are taken to be '[[First-class object|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>.<!---Notational conventions should be explained elsewhere in this article; they differ by author, anyway:---In lambda calculus, function application is regarded as [[Operator associativity|left-associative]], so that <math>stx</math> means <math>(st)x</math>.--->

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

==== Alpha equivalence ====
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 variables ====
The ''free variables''{{efn|free variables in lambda Notation and its Calculus are comparable to [[Free variables and bound variables|linear algebra and mathematical concepts of the same name]]}} 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 theory|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 theory|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 substitutions ====
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 variable|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 and bound variables|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.

==== β-reduction ====
The β-reduction rule{{efn|name=beta}} 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,{{anchor|betaReducIsAcomput}} β-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.

{{anchor|untypedData}}Another 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 value]]s, strings, or other non-number objects.