[Haskell-cafe] Associative Commutative Unification

John D. Ramsdell ramsdell0 at gmail.com
Fri Jul 11 08:39:28 EDT 2008

> Are you aware of "Term Rewriting and all That"? It describes how to do
> associative commutative unification; whether it satisfies your
> 'obviously correct' criterion I don't know.

Oh yes, I know about term rewriting.  If your equations can be
expressed as a set of confluent rewrite rules, one can use the
Martelli and Montanari's formalization of unification to come up with
an obviously correct equational unifier.  Alas, that simple trick
doesn't work for AC unification.

Have you heard of Maude?  I hear the next version will have support
for AC unification.  If I stay with Haskell, I'd have to use their
support via interprocess communication.  Yuck.



More information about the Haskell-Cafe mailing list