term rewriting system
term rewriting system (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 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. (1) The term rewriting system (Σ,E) is complete if the reduction system →E 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.
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. (1) The term rewriting system (Σ,E) is complete if the reduction system →E 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.
More From encyclopedia.com
Rendle-Short, John , René •Manet • carnet •nota bene, René •Binet • estaminet •gratiné, matinée •cloisonné, donnée, Dubonnet, Monet •Mornay • panettone • Chardonnay •Hogm… Puree , pu·rée / pyoŏˈrā; -ˈrē/ • n. a smooth, creamy substance made of liquidized or crushed fruit or vegetables: stir in the tomato purée. • v. (pu·rées ,… Principe , Príncipe •frappé • jaspé •épée, Pepe •Príncipe •coupé, Nupe, toupée •agape • canapé System , sys·tem / ˈsistəm/ • n. 1. a set of connected things or parts forming a complex whole, in particular: ∎ a set of things working together as parts of… Systems Analysis , During the normal course of doing business, companies engaging in e-commerce are faced with a wide variety of challenges or problems. These vary depe… Expert Systems , Expert systems, also called "rule-based systems," are computer programs or sets of programs that use knowledge of a domain (a specific field or disci…
You Might Also Like
NEARBY TERMS
term rewriting system