Reduction Systems - Term Rewriting Systems

Term Rewriting Systems

A term rewriting system (TRS) is a rewriting system where the objects are terms, or expressions with nested sub-expressions. For example, the system shown under Logic above is a term rewriting system. The terms in this system are composed of binary operators and and the unary operator . Also present in the rules are variables, which are part of the rules themselves rather than the term; these each represent any possible term (though a single variable always represents the same term throughout a single rule).

The term structure in such a system is usually presented using a grammar. In contrast to string rewriting systems, whose objects are flat sequences of symbols, the objects of a term rewriting system form a term algebra, which can be visualized as a tree of symbols, the structure of the tree fixed by the signature used to define the terms.

The system given under Logic above is an example of a term rewriting system.