Editing Lambda calculus (section)

== Reduction ==
The meaning of lambda expressions is defined by how expressions can be reduced.<ref>{{cite journal|last1=de Queiroz|first1=Ruy J. G. B.|author1-link=Ruy de Queiroz|year=1988|doi=10.1111/j.1746-8361.1988.tb00919.x|title=A Proof-Theoretic Account of Programming and the Role of Reduction Rules|journal=Dialectica|volume=42|issue=4|pages=265–282}}</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.

{{anchor|redex}}The 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''].{{efn|name=beta}}

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

=== α-conversion ===
'''α-conversion''' ([[alpha]]-conversion), sometimes known as α-renaming,<ref>{{Citation|title=Design concepts in programming languages|last1=Turbak|first1=Franklyn|last2=Gifford|first2=David|year=2008|publisher=MIT press|page=251|isbn=978-0-262-20175-9}}</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 (programming languages)|name resolution]] simpler by ensuring that no variable name [[Variable shadowing|masks]] a name in a containing [[scope (programming)|scope]] (see [[Name resolution (programming languages)#Alpha renaming to make name resolution trivial|α-renaming to make name resolution trivial]]).

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

==== Substitution ====
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''<sub>1</sub> ''M''<sub>2</sub>)[''x'' := ''N''] = ''M''<sub>1</sub>[''x'' := ''N''] ''M''<sub>2</sub>[''x'' := ''N'']
: (λ''x''.''M'')[''x'' := ''N''] = λ''x''.''M''
: (λ''y''.''M'')[''x'' := ''N''] = λ''y''.(''M''[''x'' := ''N'']), if ''x'' ≠ ''y'' and ''y'' ∉ FV(''N'')  ''See [[#Free and bound variables|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 [[#Capture-avoiding substitutions|above]]''.

=== β-reduction ===
'''β-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''].{{efn|name= beta}}

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

=== η-conversion ===
'''η-conversion''' ([[eta]] conversion) expresses the idea of [[extensionality]],<ref name= etaReduct >Luke Palmer [https://mail.haskell.org/pipermail/haskell-cafe/2010-December/087783.html (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]].