[Haskell-cafe] Associative Commutative Unification

[Pepe Iborra]

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.
>
> http://maude.cs.uiuc.edu/
>
> John
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at 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/