# $\beta$-reduction

## Idea

In type theory, $\beta$-reduction is a process of “computation”, which generally replaces more complicated terms with simpler ones. It was originally identified in the lambda-calculus, where it contrasts with $\alpha$-equivalence and $\eta$-expansion; this is the version described below for function types. The analogous reduction for inductive types may also be known as $\iota$-reduction.

## “Definition”

In its most general form, $\beta$-reduction consists of rules which specify, for any given type $T$, if we apply an “eliminator” for $T$ to the result of a “constructor” for $T$, how to “evaluate” the result. We write

$s{\to }_{\beta }t$s \to_\beta t

if the term $s$ beta-reduces to the term $t$. Sometimes we write $s{\to }_{\beta }^{*}t$ if this reduction takes $n$ steps (leaving off the $*$ to denote $n=1$). The relation “reduces to” generates an equivalence relation on the set of terms called beta equivalence and often denoted $s{=}_{\beta }t$ or $s{\equiv }_{\beta }t$.

### Function types

The most common (and original) example is when $T$ is a function type $A\to B$.

In this case, the constructor of $A\to B$ is a $\lambda$-expression: given a term $b$ of type $B$ containing a free variable $x$ of type $A$, then $\lambda x.\phantom{\rule{thinmathspace}{0ex}}b$ is a term of type $A\to B$.

The eliminator of $A\to B$ says that given a term $f$ of type $A\to B$ and a term $a$ of type $A$, we can apply $f$ to $a$ to obtain a term $f\left(a\right)$ of type $B$.

Now if we first construct a term $\lambda x.\phantom{\rule{thinmathspace}{0ex}}b:A\to B$, and then apply this term to $a:A$, we obtain a term $\left(\lambda x.\phantom{\rule{thinmathspace}{0ex}}b\right)\left(a\right):B$. The rule of $\beta$-reduction then tells us that this term evaluates or computes or reduces to $b\left[a/x\right]$, the result of substituting the term $a$ for the variable $x$ in the term $b$.

See lambda calculus for more.

### Product types

Although function types are the most publicized notion of $\beta$-reduction, basically all types in type theory have a form of it. For instance, in the negative presentation of a product type $A×B$, the constructor is an ordered pair $\left(a,b\right):A×B$, while the eliminators are projections ${\pi }_{1}$ and ${\pi }_{2}$ which yield elements of $A$ or $B$.

The beta reduction rules then say that if we first apply a constructor $\left(a,b\right)$, then apply an eliminator to this, the resulting terms ${\pi }_{1}\left(a,b\right)$ and ${\pi }_{2}\left(a,b\right)$ compute to $a$ and $b$ respectively.

Revised on August 13, 2012 22:07:38 by Mike Shulman (71.136.235.154)