Overview

abstract reduction system


Show Summary Details

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,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.

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

[...]

Subjects: Computing.


Reference entries

Users without a subscription are not able to see the full content. Please, subscribe or login to access all content.