Abstract Reduction System

Definition

An abstract reduction system is a pair $(A,\to )$ consisting of a set or class $A$ of objects together with a binary relation $\to$ on $A$. The objects need not be terms: they may be proofs, graphs, machine states, or any other entities on which one studies computation or simplification.

The judgement $a\to b$ means that $a$ reduces to $b$ in one step.

Reduction Sequences

From the one-step relation one forms the usual derived relations:

• $a{\to }^{\ast }b$: $b$ is reachable from $a$ by zero or more reduction steps
• $a{\to }^{+}b$: $b$ is reachable from $a$ by one or more reduction steps
• $a{\leftrightarrow }^{\ast }b$: $a$ and $b$ are inter-convertible by reductions and reverse reductions

These derived relations are the setting in which one studies confluence, normal forms, and normalization.

Remarks

The abstract viewpoint isolates the structural theory of reduction from any particular syntax. A term rewriting system is a common source of an abstract reduction system, but the basic notions of reduction theory do not depend on terms in particular.

Related Concepts

Reduction
Reduction Rule
Normal Form
Confluence
Church-Rosser Property
Strong Normalization
Weak Normalization
Convergent (Rewriting)
Term Rewriting System

References

baader1998-term-rewriting