The λ calculus consists of a single transformation rule (variable substitution) and a single function definition scheme. It was introduced in the 1930s by Alonzo Church as a way of formalizing the concept of effective computability. The λ calculus is universal in the sense that any computable function can be expressed and evaluated using this formalism.


<expression>  := <name> | <function> | <application>  
<function>    := λ <name>.<expression>  
<application> := <expression><expression>  

A “name”, also called a “variable”, is an identifier which can be any of the letters a, b, c, . . .
The only keywords used in the language are λ and the dot .

λx.x An example of a function

This expression defines the identity function. The name after the λ is the identifier of the argument of this function. The expression after the dot (in this case a single x) is called the body of the definition.
Functions can be applied to expressions: such as (λx.x)y, This is the identity function applied to y. Function applications are evaluated by substituting the value of the argument x (in this case y) in the body of the function definition, (λx.x)y = [y/x]x = y

Free and bound variables

we say that a variable name is free in an expression if one of the following three cases holds:

  • name is free in name.
  • name is free in λname1.exp if the identifier name!=name1 and name is free in exp.
  • nameis free in E1E2 if name is free in E1 or if it is free in E2.

And is bound if one of two cases holds:

  • name is bound in λname1.exp if the identifier name=name1 or if name is bound in exp.
  • name is bound in E1E2 if name is bound in E1 or if it is bound in E2.