[Haskell-cafe] Associative Commutative Unification

[John D. Ramsdell]

> 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.

http://maude.cs.uiuc.edu/

John