Editing Lambda calculus (section)

==== Lambda terms ====
The syntax of the lambda calculus defines some expressions as valid lambda calculus expressions and some as invalid, just as some strings of characters are valid computer programs and some are not. A valid lambda calculus expression is called a "'''lambda term'''".

The following three rules give an [[inductive definition]] that can be applied to build all syntactically valid lambda terms:{{efn|name=lamTerms|1= The expression e can be:   variables x, lambda abstractions, or applications —in BNF, <math>e ::= x \mid \lambda x.e \mid e \, e</math> .— ''from Wikipedia's [[Simply typed lambda calculus#Syntax]] for untyped lambda calculus}}
*{{anchor|validLambdaVar}} variable {{mvar|x}} is itself a valid lambda term.
*if {{mvar|t}} is a lambda term, and {{mvar|x}} is a variable, then <math>(\lambda x.t)</math>{{efn| <math>(\lambda x.t)</math> is sometimes written in [[ASCII]] as <math>L x.t</math>}} is a lambda term (called an ''abstraction'');
*if {{mvar|t}} and {{mvar|s}} are lambda terms, then <math>(t s)</math> is a lambda term (called an ''application'').
Nothing else is a lambda term. That is, a lambda term is valid if and only if it can be obtained by repeated application of these three rules. For convenience, some parentheses can be omitted when writing a lambda term. For example, the outermost parentheses are usually not written. See [[#Notation|§ Notation]], below, for an explicit description of which parentheses are optional. It is also common to extend the syntax presented here with additional operations, which allows making sense of terms such as <math>\lambda x.x^2.</math> The focus of this article is the pure lambda calculus without extensions, but lambda terms extended with arithmetic operations are used for explanatory purposes.

{{anchor|lambdaAbstr}} An ''abstraction'' <math>\lambda x.t</math> denotes an [[#anonymousForm|§ anonymous function]]{{efn|The lambda term <math>(\lambda x.t)</math> represents the function <math>x \mapsto t</math> written in anonymous form.}} that takes a single input {{mvar|x}} and returns {{mvar|t}}. For example, <math>\lambda x.(x^2+2)</math> is an abstraction representing the function <math>f</math> defined by <math>f(x) = x^2 + 2,</math> using the term <math>x^2+2</math> for {{mvar|t}}. The name <math>f</math> is superfluous when using abstraction. The syntax <math>(\lambda x.t)</math> [[Free variables and bound variables|binds]] the variable {{mvar|x}} in the term {{mvar|t}}. The definition of a function with an abstraction merely "sets up" the function but does not invoke it.

{{anchor|anApplic}} An ''application'' <math>t s</math> represents the application of a function {{mvar|t}} to an input {{mvar|s}}, that is, it represents the act of calling function {{mvar|t}} on input {{mvar|s}} to produce <math>t(s)</math>.

A lambda term may refer to a variable that has not been bound, such as the term <math>\lambda x.(x+y)</math> (which represents the function definition <math>f(x) = x + y</math>). In this term, the variable {{mvar|y}} has not been defined and is considered an unknown. The abstraction <math>\lambda x.(x+y)</math> is a syntactically valid term and represents a function that adds its input to the yet-unknown {{mvar|y}}.

Parentheses may be used and might be needed to disambiguate terms. For example, 
#{{anchor|Example1parenRightIsAbstraction}}<math>\lambda x.((\lambda x.x)x)</math> is of form <math>\lambda x.B</math> and is therefore an abstraction, while
#<math>(\lambda x.(\lambda x.x)) x</math> is of form <math>M N</math> and is therefore an application.

The examples 1 and 2 denote different terms, differing only in where the parentheses are placed. They have different meanings: example 1 is a function definition, while example 2 is a function application. The lambda variable {{mvar|x}} is a placeholder in both examples.

Here, [[#Example1parenRightIsAbstraction|example 1]] ''defines'' a function <math>\lambda x.B</math>, where <math>B</math> is <math>(\lambda x.x)x</math>, an anonymous function <math>(\lambda x.x)</math>, with input <math>x</math>; while example 2, <math>M </math>&nbsp;<math>N</math>, is M applied to N, where <math>M</math> is the lambda term <math>(\lambda x.(\lambda x.x))</math> being applied to the input <math>N</math> which is <math>x</math>. Both examples 1 and 2 would evaluate to the [[identity function]] <math>\lambda x.x</math>.