Lambda Calculus

computation lambda-calculus

Definition

Lambda Calculus

The lambda calculus is the language of expressions $e\in \mathcal{E}$ in variables $x\in \mathcal{V}$ given by the grammar:

$$e::=x\mid e{e}^{\prime }\mid \lambda x.e$$

Abstraction

Definition

Lambda Abstraction

The syntactic construct $\lambda x.e$ is called a lambda abstraction, where $x$ is a bound variable and $e$ is an expression.

todo

Link to original

Reductions

$\alpha$-Reduction

Definition

Alpha Reduction

The process of renaming bound variables is called alpha reduction (provided it doesn’t cause name conflicts).

$$\lambda u.e\equiv \lambda v.[v/u]e$$

Link to original

$\beta$-Reduction

Definition

Beta Reduction

The beta reduction relation is defined as the least congruence relation on expressions $e$ such that:

$$(\lambda x.e_1)e_2\to [e_2/x]e_1$$

where $[t/x]$ means substituting the term $t$ for each free occurrence of $x$ in $e$. If there are free variables in $e_2$ then bound variables in $e_2$ must be renamed so that substitution does not result in the free variables in $e_2$ becoming bound. This process of renaming bound variables is called alpha reduction.

Link to original

$\eta$-Reduction

Definition

Eta Reduction

An eta reduction ensures that functions providing the same results for the same arguments are equivalent.

$$\lambda v.(ev)\equiv ev\notin FV(e)$$

Link to original