Editing Lambda calculus (section)

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