On Thu, Feb 19, 2004 at 07:50:30PM +0100, Frank Atanassow wrote:

In the near future I expect to have need of an implementation of some basic term rewriting system algorithms, most notably:

- term matching and unification - same, modulo associativity - same, modulo associativity and commutativity

The first, of course, is easy to do myself; the second, I imagine, is not too difficult but, as I hear the last is very difficult to implement halfway efficiently, I would be grateful if someone could point me to an existing Haskell implementation. (No, I could not find a pointer at the Haskell website, or by scouring the web.)

BTW, bonus points if such a framework supports extra things like checks for TRS confluence, termination, enumeration of critical pairs, Knuth-Bendix completion, etc.

There's an OCaml library at http://cime.lri.fr/ that does all this and much more, but of course in OCaml. I have a little first-order term library that does matching, rewriting, unification and completion, but not AC. It's not ready for the world yet (surprise) but I can send you a copy. It depends on your application, but instead of matching and unification modulo AC, you may be able to use completion -- associativity is fine with the standard algorithm, and AC can be handled by extended versions that rewrite with equations.