On Fri, Jul 11, 2008 at 2:39 PM, John D. Ramsdell <[EMAIL PROTECTED]> wrote: >> 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 > _______________________________________________ > 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/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe