[Haskell-cafe] Associative Commutative Unification

[John D. Ramsdell]

I'd like to write an obviously correct implementation of a unifier, a
program that when given two terms, finds a substitution that makes the
two terms equal.  The phrase "obviously correct" is meant to imply
that the clarity of the code trumps efficiency.  As near as I can
tell, high performance unifiers are full of side-effects, and
achieving the same performance without side-effects in Haskell is
difficult or impossible.

In contrast, it is easy to write obviously correct Hasklell
implementations of unifiers for freely generated term algebras.  One
can use Lawrence Paulson's code in ML for the Working Programmer as a
template or follow Martelli and Montanari's simple set of rules.

My problem is one of my operators is multiplication, which is
associative and commutative.  These two properties make unification
much more difficult.  Mark Stickel described a complete unification
algorithm for this problem, but the task of translating his
description into an obviously correct Haskell program appears to be
difficult.  For example, the algorithm requires the generation of the
basis of solutions to linear homogeneous diophantine equations.  I
haven't located an algorithm for this part yet.

If you have experience implemented equational unification in Haskell,
please share it.

John