The fundamental concept in lambda calculus is the notion if an expression. An expression is defined as
A name, also called a variable, is an identifier which, in general, can be any of the letters . For example, .
An function is defined as
An example of a function is the following
This expression defines the identity function. The name after the is the identifier or the argument of this function. The expression after the point (in this case a single ) is called the body of the function.
Functions can be applied to expressions.
An application is defined as
An example of an application is the following
This is the identity function applied to . Parenthesis are used for clarity in order to avoid ambiguity. Function applications are evaluated by substituting the value of the argument (in this case ) in the body of the function definition, i.e.
In this transformation the notation is used to indicate that all occurrences of are substituted by in the expression to the right.
Order of Evaluation
An expression can be surrounded with parenthesis for clarity, that is, if is an expression, is the same expression. The only keywords used in the language are and the dot. In order to avoid cluttering expressions with parenthesis, the convention is that function application associates from the left.
For example the expression
is evaluated applying the expressions as follows
In calculus all names are local to definitions. In the function , is bound since its occurrence in the body of the definition is preceded by . A name not preceded by a is called a free variable. In the expression
the variable is bound and is free. In the expression
The in the body of the first expression from the left is bound to the first . The in the body of the second expression is bound to the second and the is free. It is very important to notice that the in the second expression is totally independent of the in the first expression.
Be careful when performing substitutions to avoid mixing up free occurrences of an identifier with bound ones. In the expression
the function to the left contains a bound , whereas the at the right is free. Simply by renaming the bound to , this confusion is avoided