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. (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. (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. (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. (4) The reduction system →_R is strongly terminating (or strongly normalizing or Noetherian) if there does not exist an infinite chain

   $$a_0{\to }_R{\text{a}}_1{\to }_R\dots {\to }_R{\text{a}}_{\text{n}}{\to }_R\dots$$
   of reductions in A wherein
   $$a_i\ne a_{i+1}\text{for}i=0,1,2,\dots$$

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

6. (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.