On Fri, Jul 11, 2008 at 2:39 PM, 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.
John _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
You are surely aware that AC unification is much more difficult than syntactical unification. CIMe[1] might be useful to solve the generated diophantine equations. But I don't think you will be able to obtain obvious correctness, and probably performance neither. I don't know what you are planning to do, but perhaps you'd be better served by Maude than by Haskell. The Maude language is a joy to use and version 2.4 with AC unification is (expectedly) being released next week in RTA. Cheers pepe [1] - http://cime.lri.fr/