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 C 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:
- a variable,
, is itself a valid lambda term
- if
is a lambda term, and is a variable, then 
is a lambda term (called a lambda abstraction);
- if and
are lambda terms, then 
is a lambda term (called an application).
Nothing else is a lambda term. Thus a lambda term is valid if and only if it can be obtained by repeated application of these three rules. However, some parentheses can be omitted according to certain rules. For example, the outermost parentheses are usually not written. See Notation, below.
A lambda abstraction 
is a definition of an anonymous function that is capable of taking a single input and substituting it into the expression . It thus defines an anonymous function that takes and returns . For example, 
is a lambda abstraction for the function 
using the term 
for . The definition of a function with a lambda abstraction merely “sets up” the function but does not invoke it. The abstraction binds the variable in the term .
An application 
represents the application of a function to an input , that is, it represents the act of calling function on input to produce 
.
There is no concept in lambda calculus of variable declaration. In a definition such as 
(i.e. 
), the lambda calculus treats 
as a variable that is not yet defined. The lambda abstraction is syntactically valid, and represents a function that adds its input to the yet-unknown .
Bracketing may be used and may be needed to disambiguate terms. For example, 
and 
denote different terms (although they coincidentally reduce to the same value). Here the first example defines a function that defines a function and returns the result of applying x to the child-function (apply function then return), while the second example defines a function that returns a function for any input and then returns it on application of x (return function then apply).
Functions that operate on functions
In lambda calculus, functions are taken to be ‘first class values‘, so functions may be used as the inputs, or be returned as outputs from other functions.
For example, 
represents the identity function, 
, and 
represents the identity function applied to . Further, 
represents the constant function 
, the function that always returns , no matter the input. In lambda calculus, function application is regarded as left-associative, so that 
means 
.
There are several notions of “equivalence” and “reduction” that allow lambda terms to be “reduced” to “equivalent” lambda terms.
Alpha equivalence
A basic form of equivalence, definable on lambda terms, is alpha equivalence. It captures the intuition that the particular choice of a bound variable, in a lambda abstraction, does not (usually) matter. For instance, and 
are alpha-equivalent lambda terms, and they both represent the same function (the identity function). The terms and are not alpha-equivalent, because they are not bound in a lambda abstraction. In many presentations, it is usual to identify alpha-equivalent lambda terms.
(WIKIPEDIA)
