abstract reduction system

views updated

abstract reduction system (abstract rewrite sytem, or abstract replacement system) A general characterization of the process of deriving or transforming data by means of rules. It is an abstraction based primarily on examples of term rewriting systems: it is simply a reflexive and transitive binary relation →R on a nonempty set A. For a,bA, if aR b then a is said to reduce or rewrite to b.

Using this abstraction, it is easy to define a range of basic notions that play a role in computing with rules.

(1) An element aA is a normal form for →R if there does not exist b, different from a, such that aR b.

(2) The reduction system →R is Church–Rosser (or confluent) if for any aA if there are b1,b2A such that aR b1 and aR b2 then there exists cA such that b1R c and b2R c.

(3) The reduction system →R is weakly terminating (or weakly normalizing) if for each aA there is some normal form bA so that aR b.

(4) The reduction system →R is strongly terminating (or strongly normalizing or Noetherian) if there does not exist an infinite chain a0R a1R …→R anR

of reductions in A wherein aiai+1 for i = 0, 1, 2, …

(5) The reduction system →R is complete if it is Church–Rosser and strongly terminating.

(6) A reduction system is Church–Rosser and weakly terminating if, and only if, every element reduces to a unique normal form. Let ≡R denote the smallest equivalence relation on A containing →R. If →R is a Church–Rosser weakly terminating reduction system then the set NF(→R) of normal forms is a transversal for ≡R, i.e. a set that contains one and only one representative of each equivalence class.