Term Rewriting System

Definition

A term rewriting system is a presentation of an abstract reduction system whose objects are terms built from a signature. Formally, a term rewriting system is a pair $(\Sigma ,R)$ where

• $\Sigma$ is a signature of function symbols with specified arities.
• $R$ is a set of directed equations $l\to r$, called rewrite rules.

Usually one also requires that every variable occurring in $r$ already occurs in $l$, so that rules do not introduce arbitrary new variables.

Induced Reduction Relation

The rules in $R$ generate a one-step reduction relation on terms. If $l\to r$ is a rule, $\sigma$ is a substitution, and $C[-]$ is a context, then one obtains a reduction

$C[l\sigma ]\to C[r\sigma ].$

This induced relation is the object of study when proving properties such as confluence, termination, and the existence of normal forms.

Remarks

The basic metatheoretic notions of rewriting do not depend specifically on terms. For the general setting, see abstract reduction systems. Term rewriting is the important first-order instance in which the objects have explicit syntactic structure and the reduction relation is finitely presented by rules.

Related Concepts

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

References

baader1998-term-rewriting