[Haskell] AC-unification libraries?
ross at soi.city.ac.uk
Tue Feb 24 11:04:20 EST 2004
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.
More information about the Haskell