beta-reduction

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

logic | category theory | type theory |
---|---|---|

true | terminal object/(-2)-truncated object | h-level 0-type/unit type |

proposition(-1)-truncated objecth-proposition, mere proposition

proofgeneralized elementprogram

cut rulecomposition of classifying morphisms / pullback of display mapssubstitution

cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction

introduction rule for implicationunit for hom-tensor adjunctioneta conversion

logical conjunctionproductproduct type

disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)

implicationinternal homfunction type

negationinternal hom into initial objectfunction type into empty type

universal quantificationdependent productdependent product type

existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalencepath space objectidentity type

equivalence classquotientquotient type

inductioncolimitinductive type, W-type, M-type

higher inductionhigher colimithigher inductive type

completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set

setinternal 0-groupoidBishop set/setoid

universeobject classifiertype of types

modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation

proof netstring diagramquantum circuit

(absence of) contraction rule(absence of) diagonalno-cloning theorem

synthetic mathematicsdomain specific embedded programming language

</table>

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.

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$

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

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.\, 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(a)$ of type $B$.

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

See lambda calculus for more.

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 \times B$, the constructor is an ordered pair $(a,b)\colon A \times 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 $(a,b)$, then apply an eliminator to this, the resulting terms $\pi_1(a,b)$ and $\pi_2(a,b)$ compute to $a$ and $b$ respectively.

Informally, one sometimes speaks of a “$\beta$-reduction” of a definition or a proof to mean the elimination of levels of abstraction. For instance, if Theorem A is proven by invoking the existence of a green widget, which is proven by Lemma B, then a $\beta$-reduced proof of Theorem A would proceed instead by using the specific green widget constructed in the proof of Lemma B.

It makes some sense to call this $\beta$-reduction because under propositions as types, the proof of Lemma B would be a term $\lemmab:B$, whereas the proof of Theorem A would be an application $(\lambda x.\theorema)(b)$, where $\theorema$ is the proof of Theorem A using an unspecified green widget $x$. This application $(\lambda x.\theorema)(lemmab)$ can then be literally $\beta$-reduced, in the above sense, to $\theorem[lemmab/x]$, in which the specific green widget constructed in the proof of Lemma B is used instead of the unspecified one $x$.

Last revised on February 16, 2016 at 16:11:26. See the history of this page for a list of all contributions to it.