Let A be a set and
a binary relation on A.
By
we denote the special relation
.
A binary relation
is called an equivalence relation in case it is
reflexive (i.e.
), symmetric (i.e.
)
and transitive
(i.e.
).
In the following we assume that
is an equivalence relation.
For an element
we call the set
the class of
a modulo
.
Then A is a disjoint union of classes modulo
and
the set of all such classes modulo
is called the quotient of
A modulo
,
denoted by
.
A congruence on a monoid
is defined as an equivalence
relation
on the set
which is stable under left and right
multiplication with elements of
.
In particular a right (respectively left)
congruence on
is stable with respect to right
(respectively left) multiplication.
Given a congruence
on a monoid
and an element
,
we call
the
congruence class of m.
We can define a monoid structure on the set of all congruence classes
by setting
for
.
Then
is called the quotient of
by
and the homomorphism
induced by
is in fact surjective.
Congruences now provide the means to construct presentations of monoids.
A set of symbols
is called a set of generators for
under the mapping
,
if the extension of
to the set of words
on
defined by
,
is a
homomorphism from
onto
.
If for two words
we have
we say that
satisfies the relation w = w'.
The word problem for a monoid
now is to decide whether
for two words
,
satisfies the relation w = w'.
Given a set of relations R we say that a word u is
directly derivable
from an other word v under the relation
,
if either u = xly and v = xry
or u = xry and v = xly for words x,y.
We call u derivable from v under R if
there exist words
such that v= v0, vi+1 is directly derivable
from vi for
and vn = u.
Notice that if u is derivable from v under R,
then
holds, i.e. u=v is a relation
in
.
We then call the relation a consequence of the relations R.
In case all and only relations on
are consequences of the relations R we
say that
is a presentation of
defined by
.
is also called a Thue system in the literature.
Now the easiest way to give a presentation of a monoid
is to
take the set
itself as a generating set and to use the multiplication
table of
as the defining relations.
However this presentation in general will not be finite and other presentations
fulfilling additional conditions, e.g. finitely many generators of finitely
many relations, are hoped for.
In order to construct a presentation of a monoid
one has to
By Newman's lemma we know that under the hypothesis that a
reduction relation is Noetherian, a string rewriting system is confluent if
and only if it is locally confluent, i.e.,
for all u,v,w in ,
and
imply the existence of
z in
such that
and
.
For finite string rewriting systems the global property of being locally
confluent can be localized to enable a finite confluence test.
Remember that presentations of monoids can be treated as string rewriting
systems and notice that string rewriting systems are in fact presentations of monoids.
Hence, in case they are finite, convergent and effective,
we can ``compute'' in the
monoid using the irreducible elements as representatives for the
monoid elements.
The process of trying to turn a Noetherian string rewriting system into a
convergent one by resolving the not locally confluent situations is
called completion.
We will now sketch how a finite string rewriting system
presenting a monoid can
be completed in case we have a total admissible2 well-founded3
ordering
on
such that for all
we have
.
This ordering then will be called a completion ordering for T
and the completion process transforms
into a (not necessarily
finite) convergent string rewriting system presenting the same monoid.
It is important that in order to check a finite Noetherian string rewriting system
T for confluence
we only have to look at a finite set of critical situations:
for two not necessarily different rules
(l1,r1),(l2,r2) in T the set of critical pairs is
defined as
.
Now given a finite string rewriting system
with a completion ordering
we can specify a completion process as follows:
Procedure: KNUTH BENDIX COMPLETION
Given: A string rewriting system, and a total well-founded admissible ordering
. [2ex]
;
; while
do
; % Remove an element using a fair strategy for all critical pairs
do %
=
%
![]()
;
; % normal.form(z,
Since the word problem for arbitrary string rewriting systems is undecidable, this procedure in general will not terminate. Nevertheless, using a fair4 strategy to remove elements from the set B, it always enumerates a convergent string rewriting system based on the completion ordering
presenting the same monoid as the input system.
![]()
![]()
![]()
Next: 3. Relating the Word Up: Relating Rewriting Techniques on Previous: 1. Introduction | ZCA Home | Reports |