Definition

A term rewriting system, or more generally an abstract reduction system, is convergent if it is both strongly normalizing and confluent.

In rewriting terminology, this is often phrased as “terminating and confluent”.

Consequences

In a convergent system, every object reduces to a unique normal form. This makes reduction into a decision procedure for equality modulo the induced rewrite theory, provided the reduction relation is effectively computable.

Strong Normalization
Confluence
Normal Form
Term Rewriting System

References

baader1998-term-rewriting