TOPICS
Search

Reduction System


A system in which words (expressions) of a formal language can be transformed according to a finite set of rewrite rules is called a reduction system. While reduction systems are also known as string rewriting systems or term rewriting systems, the term "reduction system" is more general.

Lambda calculus is an example of a reduction system with lambda conversion rules constituting its rewrite rules.

If none of the rewrite rules of a reduction system apply to expression E, then E is said to be in normal form for a reduction system.

A pair of expressions (x,y) is called joinable if both x and y can be reduced to the same expression in zero or more reduction steps (i.e., applications of rewrite rules).

If x is reduced to y in one step, this is indicated x->y. If x is reduced to y in zero or more steps, this is indicated x->_*y. The notation x<->_*y is used if there is a sequence {a_0,...,a_n} such that a_0=x, a_n=y, and for every pair (a_i,a_(i+1)), either a_i->a_(i+1) or a_(i+1)->a_i.


See also

Church-Rosser Property, Confluent, Critical Pair, Finitely Terminating, Formal Language, Knuth-Bendix Completion Algorithm, Lambda Calculus, Multiway System, Reduction Order, 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

Reduction System

Cite this as:

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

Subject classifications