## Quick Reference

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*→

*b then*

_{R}*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.*a* ∈ *A* is a **normal form** for →* _{R}* if there does not exist

*b*, different from

*a*, such that

*a*→

*b.*

_{R}*is*

_{R}**Church-Rosser**(or

**confluent**) if for any

*a*∈

*A*if there are

*b*

_{1},

*b*

_{2}∈

*A*such that

*a*→

*b*

_{R}_{1}and

*a*→

*b*

_{R}_{2}then there exists

*c*∈

*A*such that

*b*

_{1}→

*c and*

_{R}*b*

_{2}→

*c.*

_{R}*is*

_{R}**weakly terminating**(or

**weakly normalizing**) if for each

*a*∈

*A*there is some normal form

*b*∈

*A*so that

*a*→

*b.*

_{R}*is*

_{R}**strongly terminating**(or

**strongly normalizing**or

**Noetherian**) if there does not exist an infinite chain

*a*

_{0}→

*a*

_{R}_{1}→

*…→*

_{R}*a*

_{R}_{n}→

*… of reductions in*

_{R}*A*wherein

*a*

*≠*

_{i}*a*

_{i}_{+1}for

*i*= 0, 1, 2, …

*is*

_{R}**complete**if it is Church—Rosser and strongly terminating.

**unique**normal form. Let ≡

*denote the smallest equivalence relation on*

_{R}*A*containing →

*. If →*

_{R}*is a Church-Rosser weakly terminating reduction system then the set*

_{R}*NF*(→

*) of normal forms is a transversal for ≡*

_{R}*, i.e. a set that contains one and only one representative of each equivalence class.*

_{R}*a* ∈ *A* is a **normal form** for →* _{R}* if there does not exist

*b*, different from

*a*, such that

*a*→

*b.*

_{R}* _{R}* is

**Church-Rosser**(or

**confluent**) if for any

*a*∈

*A*if there are

*b*

_{1},

*b*

_{2}∈

*A*such that

*a*→

*b*

_{R}_{1}and

*a*→

*b*

_{R}_{2}then there exists

*c*∈

*A*such that

*b*

_{1}→

*c and*

_{R}*b*

_{2}→

*c.*

_{R}* _{R}* is

**weakly terminating**(or

**weakly normalizing**) if for each

*a*∈

*A*there is some normal form

*b*∈

*A*so that

*a*→

*b.*

_{R}* _{R}* is

**strongly terminating**(or

**strongly normalizing**or

**Noetherian**) if there does not exist an infinite chain

*a*

_{0}→

*a*

_{R}_{1}→

*…→*

_{R}*a*

_{R}_{n}→

*… of reductions in*

_{R}*A*wherein

*a*

*≠*

_{i}*a*

_{i}_{+1}for

*i*= 0, 1, 2, …

* _{R}* is

**complete**if it is Church—Rosser and strongly terminating.

**unique** normal form. Let ≡* _{R}* denote the smallest equivalence relation on

*A*containing →

*. If →*

_{R}*is a Church-Rosser weakly terminating reduction system then the set*

_{R}*NF*(→

*) of normal forms is a transversal for ≡*

_{R}*, i.e. a set that contains one and only one representative of each equivalence class.*

_{R}[...]

*Subjects:*
Computing.