35.1 Operations on rewriting systems

This is the category in which all rewriting systems lie.

The rules comprising the rewriting system. Note that these may change through the life of the rewriting system, however they will always be a set of defining relations of the algebra described by the rewriting system.

The order of the rewriting system.

Given an element u in the free (or term) algebra over which rws is defined, rewrite u by successive applications of the rules of rws until no further rewriting is possible, and return the resulting element of T.

Checks whether the rewriting system rws is confluent. A rewriting system is confluent if, for every two words u and v in the free algebra T which represent the same element of the algebra A defined by rws, ReducedForm(rws,u) = ReducedForm(rws,v) as words in the free algebra T. This element is the unique normal form of the element represented by u.

In its second form, if A is an algebra with a canonical rewriting system associated with it, it checks whether that rewriting system is confluent.

Return a new rewriting system defining the same algebra as rws which is confluent.

A rewriting system is reduced if for each rule (l, r), l and r are both reduced.

Reduce rules and remove redundant rules to make rws reduced.

Add rule to a rewriting system rws.

Add rule to rewriting system rws. Performs a reduction operation on the resulting system, so that if rws is reduced it will remain reduced.

Add rules (and perhaps reduce) in order to make rws confluent

[Top] [Up] [Next] [Index]