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.