Finitely terminating rewriting system

Definition

Symbol-free definition

A rewriting system is said to be finitely terminating if every chain of reductions in the rewriting system terminates in finitely many steps.

Note that though this property is originally defined for a rewriting system of a monoid, it also makes sense for a rewriting system for a group.

Relation with other properties

Stronger properties

• Special rewriting system
• Monadic rewriting system
• Length-reducing rewriting system

Weaker properties

• Boundedly terminating rewriting system
• Linear-time terminating rewriting system