A reduction system is called finitely terminating (or Noetherian) if there are no infinite rewriting sequences. This property guarantees that any rewriting algorithm will terminate on any input.
Ordering expressions may help to find out that a reduction system is finitely terminating. Orders used for this purpose are based on some measure of expression complexity. Existence of a reduction order compliant with rules of a term rewriting system guarantees that the system is finitely terminating.
The problem of determining whether a given reduction system is finitely terminating is recursively undecidable.
