Linear-time terminating rewriting system

Definition

Symbol-free definition

A rewriting system is said to be linear-time terminating if there is a positive constant $c$ such that the length of any chain beginning with a word of length $n$, is not more than $cn$.

Relation with other properties

Stronger properties

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

Weaker properties

• Finitely terminating rewriting system