[sci.math.symbolic] making rules out of equations

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

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 -

usenet: bylund@cs.umu.se
		``Capacity to Terminate
		  Is a Specific Grace''
    				-E Dickinson