# 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:

\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 functionx => 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);
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: