Editing Lambda calculus (section)

=== Free and bound variables ===
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:
# {{math|1=FV(''x'') = {{mset|''x''}}}}, where ''x'' is a variable.
# {{anchor|FreeMsExXs}} {{math|1=FV(''λx''.''M'') = FV(''M'') \ {{mset|''x''}}}}.{{efn|The set of free variables of M, but with {''x''} removed}}
# {{anchor|FreeMsNs}} {{math|1=FV(''M N'') = FV(''M'') ∪ FV(''N'').}}{{efn|The union of the set of free variables of <math>M</math> and the set of free variables of <math>N</math><ref name="BarendregtBarendsen">{{Citation|last1=Barendregt|first1=Henk|author1-link=Henk Barendregt|last2=Barendsen|first2=Erik|title=Introduction to Lambda Calculus|date=March 2000|url=https://ftp.science.ru.nl/CSI/CompMath.Found/lambda.pdf}}</ref>}}

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