TOPICS
Search

Finitely Terminating


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.


See also

Church-Rosser Property, Confluent, Critical Pair, Knuth-Bendix Completion Algorithm

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

References

Baader, F. and Nipkow, T. Term Rewriting and All That. Cambridge, England: Cambridge University Press, 1999.

Referenced on Wolfram|Alpha

Finitely Terminating

Cite this as:

Sakharov, Alex. "Finitely Terminating." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/FinitelyTerminating.html

Subject classifications