**bylund@cs.umu.se (Stefan Bylund)** (11/16/90)

Hi - The subject is *completion modulo equations*, and *rewriting modulo rules and equations*. I have found this computational model (term rewriting systems (TRS)) *very* interesting since, well, I would say it's on its way to become a new `paradigm' (oh, it already is? :-) in the computer science community. The model is nondeterministic in itself, and a *lot* of basic applications is known, e g in code generation systems, code optimizers, rule based systems, appl in kbs's,..., the list can be made arbitrary long. We simply construct minimal desicion procedures out of arbitrary sets of axioms. The basic problems is: o the minimal construction of certain *critical pairs* out of two rules modulo some equational theory E o and when we have our rules (made up from equations), what kind of rewriting relation should we use to effectively compute normal forms o estimation of the complexity of the algorithms used in the above o lots of more... I now wonder what the appropriate groups are for discussing issues in the TRS field. In particular, I would like to discuss a (well-known ?) article by Jouannaud and Kirchner - ``Completion of a set of rules modulo a set of equations'' in SIAM J Comput. Vol. 15, No. 4, Nov 1986. I have found several ``vague'' things when trying to implement the algorithm in that paper, e g (think tex!) o firstly, speaking of the reduction relation used, we should use ->^{R^E} \subset ->^{R,E} \subset (~ \circ ->^R), but what *exactly* should ->^R^E be? Is that a matter of feeling? o any good algorithms for the ``matching'' problem published anywhere? I am currently mostly interested in the theory of Associative and Commutative (AC) operators, and during the rewriting of a term t we need to AC-match the left hand side of a rule l->r with t (and hopefully without matching l with *every* constructable permutation of t.) o more, which may rain if responses is gained from the above. Another group? Comments? Anyone? Thanks - -stefan -- usenet: bylund@cs.umu.se ``Capacity to Terminate Is a Specific Grace'' -E Dickinson