## Quick Reference

(TRS)

A formal system for manipulating terms over a signature by means of rules. A set *R* of rules (each a rewrite rule) creates an abstract reduction system →* _{R}* on the algebra

*T*(Σ,

*X*) of all terms over signature Σ and variables

*X*. Usually, the rules are a set

*E*of equations that determine a reduction system →

*using rewrites based on equational logic.*

_{E}Let *E* be a set of equations such that, for each *t*=*t*′ ∈ *E*, the left-hand side *t* is not a variable. The pair (Σ,*E*) is called an **equational TRS**. The equations of *E* are used in derivations of terms where the reduction *t* →_{E}*t*′ requires substitutions to be made in some equation *e* ∈ *E* and the left-hand side of *e* is replaced by the right-hand side of *e* in *t* to obtain *t*′.

The first set of properties of a term rewriting system (Σ,*E*) is now obtained from the properties of abstract reduction systems. The following are examples.*E*) is **complete** if the reduction system →* _{R}* on

*T*(Σ) is Church-Rosser and strongly terminating.

*be the smallest congruence containing →*

_{E}*and*

_{E}*T*(Σ,

*E*) be the factor algebra

*T*(Σ)|≡

*. Then*

_{E}*T*(Σ,

*E*) is the initial algebra of Alg(Σ,

*E*). If (Σ,

*E*) is a finite equational TRS specification that is complete, then

*T*(Σ,

*E*) is a computable algebra.See also orthogonal term rewriting system.

*E*) is **complete** if the reduction system →* _{R}* on

*T*(Σ) is Church-Rosser and strongly terminating.

* _{E}* be the smallest congruence containing →

*and*

_{E}*T*(Σ,

*E*) be the factor algebra

*T*(Σ)|≡

*. Then*

_{E}*T*(Σ,

*E*) is the initial algebra of Alg(Σ,

*E*). If (Σ,

*E*) is a finite equational TRS specification that is complete, then

*T*(Σ,

*E*) is a computable algebra.

*Subjects:*
Computing.

## Related content in Oxford Index

##### Reference entries

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.