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. Thanks in advance. Regards, Frank