[Haskell] AC-unification libraries?

[Ross Paterson]

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.