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

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** $\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)$

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.

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:

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