Skip to main content

Lambda Calculus (Computer Science)

Lambda Calculus is a formal definition for expressing functional computational operations based on variable binding and substitution.

It was introduced by Alonzo Church resulting from his studies on the foundation of mathematics and computation.



The set of λ\lambda-calculus terms is defined by

t::= x t1t2 (t)  λ ::= \space x | \space t_1 t_2 | \space (t) \space | \space \lambda x.t

A term can be a variable (e.g., xx), the application of one term t1t_1 to another term t2t_2, and an abstraction of a variable from a term tt. Furthermore, the λ\lambda-calculus allows for using parentheses for structuring terms.


(t1 t2)(t_1 \space t_2) is an application. It is the application of the term t1t_1 to an argument t2t_2.


λx.t\lambda x.t is an abstraction and represents a bound function with the parameter xx and the function body tt. xx is bound in tt.

λx.t\lambda x.t is also called an anonymous function. It has no name and is simply defined through the formal parameter x, prefixed with the λ\lambda-symbol. A dot . separates the formal parameter from the function body tt. If tt contains an xx, this xx is bound to the formal parameter xx.

Figure 1 This λ-abstraction represents a function that returns the sum of x and 1, whereas x is the formal parameter and bound in the term t.

Sequences of formal parameters may be collapsed:

λx.λy.λz.tλxyz.t\lambda x. \lambda y . \lambda z . t \lrArr \lambda xyz.t


The anonymous function from above can be implemented in Haskell:

\x -> x + 1

The leading backslash ought to remind one of the Lambda-symbol: "In Haskell source code, the Greek letter lambda is replaced by a backslash character ('\') instead [...]" [Haskell Wiki]

In JavaScript, the anonymous function can be implemented like this:

// traditional
(function(x) {return x + 1;})

// arrow function
x => x + 1

Bound Variables

In a Lambda term λx.t\lambda x.t we call the formal parameter λx\lambda x the binder, and say that the subterm tt is in the scope of the binder: Occurrences of xx in tt are bound.

In an informal sense, xx is a local variable in the function-body tt.

The set of Bound Variables in a Lambda Calculus-term are defined by:

BV(x)=BV(x) = \empty

BV(t1 t2)=BV(t1)BV(t2)BV(t_1 \space t_2) = BV(t_1) \cup BV(t_2)

BV(λx.t)=xBV(t)BV(\lambda x . t) = {x} \cup BV(t)

bound variables in mathematics

In mathematics, bound variables are also known:

x=15x\displaystyle\sum_{x=1}^5 x

Free Variables

The set of Free Variables in a Lambda Calculus-term are defined by:

FV(x)={x}FV(x) = \{x\}: x is a free variable.

FV(t1 t2)=FV(t1)FV(t2)FV(t_1 \space t_2) = FV(t_1) \cup FV(t_2): The free variables in the application are the union of all free variables of all sub-terms.

FV(λx.t)=FV(t){x}FV(\lambda x.t) = FV(t) \setminus \{x\}: The free variables in the abstraction are the free variables of the body of the abstraction, minus any variable bound by the parameters of the abstraction.


A free variable is a variable that is not bound in a term tt. The following would implement an anonymous function where the variable xx is bound in the function body, and yy is a free variable:

const y = 1;

(x => x + y)(5);
let y = 1

(\x -> x + y)(5)


Lambda calculus-terms can be brought into β\beta-normal-form by applying β\beta-reduction - that is, informal, evaluating a term by applying arguments to it.

(λx.s)ts[x:=t](\lambda x.s) t \rarr s[x:=t]

Here, λx.s\lambda x.s is a term that gets applied to another term tt, and is called the β\beta-redex. It gets reduced to s[x:=t]s[x:=t], the reduct: All occurrences of xx in ss are replaced with tt.

Figure 2


  • The β\beta-normal-form of (λx.x)(λy.y)(\lambda x.x)(\lambda y.y) is

(λx.x)(λy.y)βλy.y(\lambda x.x)(\lambda y.y) \rarr_\beta \lambda y.y

  • The β\beta-normal-form of (λx.z)((λy.y)(λω.ω))(\lambda x.z)((\lambda y.y)(\lambda \omega.\omega)) is

(λx.z)((λy.y)(λω.ω))β(λx.z)(λω.ω)(\lambda x.z)(\underline{(\lambda y.y)(\lambda \omega.\omega)}) \rarr_\beta (\lambda x.z)(\underline{\lambda \omega.\omega})

(λx.z)(λω.ω)βz(\lambda x.z)(\underline{\lambda \omega.\omega}) \rarr_\beta z