Editing Lambda calculus (section)

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