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. _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
