abstract reduction system

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,b ∈ A, if a →_R 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 a ∈ A is a normal form for →_R if there does not exist b, different from a, such that a →_R b.

(2) The reduction system →_R is Church–Rosser (or confluent) if for any a ∈ A if there are b₁,b₂ ∈ A such that a →_R b₁ and a →_R b₂ then there exists c ∈ A such that b₁ →_R c and b₂ →_R c.

(3) The reduction system →_R is weakly terminating (or weakly normalizing) if for each a ∈ A there is some normal form b ∈ A so that a →_R b.

(4) The reduction system →_R is strongly terminating (or strongly normalizing or Noetherian) if there does not exist an infinite chain a₀ →_R a₁ →_R …→_R a_n →_R …

of reductions in A wherein a_i ≠ a_i+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.