Elimination Rule

Definition

An elimination rule in Type Theory specifies how to use or decompose values of a given type. Elimination rules describe what operations can be performed on elements of a type to extract information or produce values of other types.

Elimination rules are dual to introduction rules: while introduction rules construct values of a type, elimination rules destruct or consume them.

General Form

For a type $T$, an elimination rule typically has the form:

$\frac{t:T\text{(additional premises)}}{e(t):U}$

This states that given $t:T$ (and possibly other premises), we can apply eliminator $e$ to produce a value of type $U$.

Examples

Product Type Elimination

For Product Type $A\times B$, the elimination rules are projections:

$\frac{p:A\times B}{{\pi }_1(p):A}\frac{p:A\times B}{{\pi }_2(p):B}$

Function Type Elimination

For Function Type $A\to B$, the elimination rule is function application:

$\frac{f:A\to Ba:A}{f(a):B}$

Sum Type Elimination

For Sum Type $A+B$, the elimination rule is case analysis:

$\frac{s:A+Bf:A\to Cg:B\to C}{\text{case}(s,f,g):C}$

Natural Numbers Elimination

For natural numbers $\mathbb{N}$, the elimination rule is recursion/induction:

$\frac{n:\mathbb{N}z:Cs:\mathbb{N}\to C\to C}{\text{rec}(n,z,s):C}$

Relationship to Computation

Elimination rules interact with introduction rules via computation rules (β-rules) that specify how eliminators reduce when applied to introduced values.

Related Concepts

• Introduction Rule: The dual operation for constructing values
• Computation Rule: Rules governing how elimination reduces on introduced values
• Type Theory: The formal system in which these rules are defined
• Product Type: Example type with projection eliminators
• Function Type: Example type with application eliminator
• Sum Type: Example type with case analysis eliminator