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