Editing Lambda calculus (section)

=== α-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]]''.