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 |