Overview

term rewriting system


Show Summary Details

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 →E using rewrites based on equational logic.

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 tEt′ requires substitutions to be made in some equation eE 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.(1) The term rewriting system (Σ,E) is complete if the reduction system →R on T(Σ) is Church-Rosser and strongly terminating.(2) Let ≡E be the smallest congruence containing →E and T(Σ,E) be the factor algebra T(Σ)|≡E. Then 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.

(1) The term rewriting system (Σ,E) is complete if the reduction system →R on T(Σ) is Church-Rosser and strongly terminating.

(2) Let ≡E be the smallest congruence containing →E and T(Σ,E) be the factor algebra T(Σ)|≡E. Then 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.


Reference entries

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