Editing Lambda calculus (section)

== Formal definition ==
{{Further|Lambda calculus definition}}

=== Definition ===
Lambda expressions are composed of:
* variables ''v''<sub>1</sub>, ''v''<sub>2</sub>, ...;
* the abstraction symbols λ (lambda) and . (dot);
* parentheses ().

The set of lambda expressions, {{math|Λ}}, can be [[Recursive definition|defined inductively]]:

# If ''x'' is a variable, then {{math|''x'' ∈ Λ.}}
# If ''x'' is a variable and {{math|''M'' ∈ Λ,}} then {{math|(λ''x''.''M'') ∈ Λ.}}
# If {{math|''M'', ''N'' ∈ Λ,}} then {{math|(''M N'') ∈ Λ.}}

Instances of rule 2 are known as ''abstractions'' and instances of rule 3 are known as ''applications''.<ref>{{Cite book|url= https://www.elsevier.com/books/the-lambda-calculus/barendregt/978-0-444-87508-2|last1=Barendregt|first1=Hendrik Pieter|author1-link=Henk Barendregt|title=The Lambda Calculus: Its Syntax and Semantics|publisher=North Holland|year=1984|volume=103|series=Studies in Logic and the Foundations of Mathematics|edition=Revised|isbn=0-444-87508-5}} ([https://ftp.science.ru.nl/CSI/CompMath.Found/ErrataLCalculus.pdf Corrections]).</ref> ''See [[#redex|§ reducible expression]]''

This set of rules may be written in [[Backus–Naur form]] as:
<syntaxhighlight lang="bnf">
 <expression>  ::= <abstraction> | <application> | <variable>
 <abstraction> ::= λ <variable> . <expression>
 <application> ::= ( <expression> <expression> )
 <variable>    ::= v1 | v2 | ...
</syntaxhighlight>

=== Notation ===
To keep the notation of lambda expressions uncluttered, the following conventions are usually applied:
* Outermost parentheses are dropped: ''M'' ''N'' instead of (''M'' ''N'').
* Applications are assumed to be left associative: ''M'' ''N'' ''P'' may be written instead of ((''M'' ''N'') ''P'').<ref name="lambda-bound">{{cite web|url=http://www.lambda-bound.com/book/lambdacalc/node27.html|title=Example for Rules of Associativity|publisher=Lambda-bound.com|access-date=2012-06-18}}</ref>
* When all variables are single-letter, the space in applications may be omitted: ''MNP'' instead of ''M'' ''N'' ''P''.<ref>{{cite web |title=The Basic Grammar of Lambda Expressions |url=https://softoption.us/node/33 |website=SoftOption |quote=Some other systems use juxtaposition to mean application, so 'ab' means 'a@b'. This is fine except that it requires that variables have length one so that we know that 'ab' is two variables juxtaposed not one variable of length 2. But we want to labels like 'firstVariable' to mean a single variable, so we cannot use this juxtaposition convention.}}</ref>
* The body of an abstraction extends [[Regular expression#Lazy matching|as far right as possible]]: λ''x''.''M N'' means λ''x''.(''M N'') and not (λ''x''.''M'') ''N''.
* A sequence of abstractions is contracted: λ''x''.λ''y''.λ''z''.''N'' is abbreviated as λ''xyz''.''N''.<ref name="Selinger">{{Citation|first1=Peter|last1=Selinger|title=Lecture Notes on the Lambda Calculus|year=2008|page=9|publisher=Department of Mathematics and Statistics, University of Ottawa|url=http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf|bibcode=2008arXiv0804.3434S|volume=0804|arxiv=0804.3434|issue=class: cs.LO}}</ref><ref name="lambda-bound" />

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