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.

Notation

Term

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

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

A term can be a variable (e.g., $x$), the application of one term $t_1$ to another term $t_2$, and an abstraction of a variable from a term $t$. Furthermore, the $\lambda$-calculus allows for using parentheses for structuring terms.

Application

$(t_1 \space t_2)$ is an application. It is the application of the term $t_1$ to an argument $t_2$.

Abstraction

$\lambda x.t$ is an abstraction and represents a bound function with the parameter $x$ and the function body $t$. $x$ is bound in $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 $t$. If $t$ contains an $x$, this $x$ is bound to the formal parameter $x$.

^{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:

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

info

The anonymous function from above can be implemented in Haskell:

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:

JavaScript

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

// arrow function
x => x + 1

Bound Variables

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

In an informal sense, $x$ is a local variable in the function-body $t$.

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

$BV(x) = \empty$

$BV(t_1 \space t_2) = BV(t_1) \cup BV(t_2)$

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

bound variables in mathematics

In mathematics, bound variables are also known:

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

Free Variables

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

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

$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(\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.

tip

A free variable is a variable that is not bound in a term $t$. The following would implement an anonymous function where the variable $x$ is bound in the function body, and $y$ is a free variable:

Javascript

const y = 1;

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

Haskell

let y = 1

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

β-Reduction

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.

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

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

^{Figure 2}

Examples

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

$(\lambda x.x)(\lambda y.y) \rarr_\beta \lambda y.y$

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

$(\lambda x.z)(\underline{(\lambda y.y)(\lambda \omega.\omega)}) \rarr_\beta (\lambda x.z)(\underline{\lambda \omega.\omega})$

$(\lambda x.z)(\underline{\lambda \omega.\omega}) \rarr_\beta z$

---

References:

• Tobias Nipkow, TUM: Lambda Calculus