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

Countability

Countable number of Lambda terms

There set of all possible Lambda terms is countable.

Proof

We construct a injection from $\mathcal{E}$ to $\mathbb{N}$ via a Gödel numbering. Fix an enumeration of variables $x_0,x_1,x_2,\dots$. Define the encoding $┌\cdot ┐$ recursively:

$$\begin{array}{rl}┌x_n┐& =2n\\ ┌e{e}^{\prime }┐& =2\cdot \pi (┌e┐,┌e^{\prime }┐)+1\\ ┌\lambda x_n.e┐& =2\cdot \pi (n,┌e┐)+1\end{array}$$

where $\pi :{\mathbb{N}}^2\to \mathbb{N}$ is a pairing function, which is a bijection. Each clause covers one production of the grammar $e::=x\mid e{e}^{\prime }\mid \lambda x.e$, so $┌\cdot ┐$ is well-defined and injective. Since $\mathcal{E}$ injects into $\mathbb{N}$, it is countable.