Term Rewriting System

Term rewriting systems are reduction systems in which rewrite rules apply to terms. Terms are built up from variables and constants using function symbols (or operations). Rules of term rewriting systems have the form x->y, where both x and y are terms, x is not a variable, and every variable from y occurs in x as well.

A reduction step for term r is defined as follows. If theta is a unifier for r and x, then r is reduced to ytheta. If theta is a unifier for r^' and x where r^' is a subterm of r, then r is reduced to a term obtained from rtheta by replacing r^'theta with ytheta.

See also

Church-Rosser Property, Confluent, Critical Pair, Finitely Terminating, Formal Language, Knuth-Bendix Completion Algorithm, Lambda Calculus, Multiway System, Reduction Order, Reduction System, String Rewriting System

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

Term Rewriting System

Cite this as:

Sakharov, Alex. "Term Rewriting System." From MathWorld--A Wolfram Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/TermRewritingSystem.html

Subject classifications