[Haskell-cafe] Associative Commutative Unification
mnislaih at gmail.com
Fri Jul 11 10:18:40 EDT 2008
On Fri, Jul 11, 2008 at 2:39 PM, John D. Ramsdell <ramsdell0 at gmail.com> 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
You are surely aware that AC unification is much more difficult than
CIMe 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.
 - http://cime.lri.fr/
More information about the Haskell-Cafe