Computation Rule

Definition

A computation rule (or β-rule) in Type Theory specifies how elimination forms reduce when applied to introduction forms. Computation rules describe the operational behavior of a type by defining how constructed values are deconstructed.

General Pattern

For a type with introduction form that constructs values and elimination form that destructs them, the computation rule specifies:

$\text{eliminate}(\text{introduce}(\text{components}))=\text{result computed from components}$

Examples

Product Type

For product types, the computation rules for projections are:

${\pi }_1(a,b)=a{\pi }_2(a,b)=b$

The elimination (projection) of an introduction (pairing) returns the original component.

Function Type

For function types, the β-rule for application is:

$(\lambda x.e)(a)=e[a/x]$

Applying a lambda abstraction to an argument substitutes the argument for the parameter in the body.

Sum Type

For sum types, case analysis on an injected value reduces:

$\text{case}(\text{inl}(a),f,g)=f(a)\text{case}(\text{inr}(b),f,g)=g(b)$

Natural Numbers

For natural numbers:

$\text{rec}(0,z,s)=z\text{rec}(\text{succ}(n),z,s)=s(n,\text{rec}(n,z,s))$

Purpose

Computation rules ensure that:

• Type constructors have well-defined operational semantics
• Programs can be evaluated through reduction
• The type system is decidable and normalizing
• Elimination forms are the inverse of introduction forms

Related Concepts

• Introduction Rule: Specifies how to construct values of a type
• Elimination Rule: Specifies how to use or deconstruct values of a type
• Eta Rule: The dual rule expressing uniqueness and extensionality
• Type Theory: The formal system containing these rules
• Lambda Calculus: The foundational system for β-reduction