11 Jul
2008
11 Jul
'08
8:39 a.m.
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