[TYPES] Complexity of row unification
Francois Pottier
Francois.Pottier at inria.fr
Thu Feb 17 11:18:04 EST 2005
Dear Henning,
On Sun, Feb 13, 2005 at 03:34:25AM +0000, Henning Makholm wrote:
> In the absence of such distribution it is straightforward to bound a
> pedestrian implementation of the unification algorithm by
> O(nm²*alpha(n)), where n is the size of the original equation set and
> m is the number of different labels it mentions.
This sounds about right. I don't have a proof that this is indeed an
upper bound, but I do know it is a lower bound, i.e. the standard row
unification algorithm does exhibit this behavior in the worst case.
> Unless I'm much mistaken, just a tiny bit of ingenuity will get it down to
> O(nm*alpha(n)),
Sounds plausible, although my own attempts, which involved sorting
labels, brought up an additional log(m) factor, I think.
I did not publish anything about this because I hoped to also deal with
distribution of type constructors over rows. As you mention, this made the
problem more difficult, and I did not come up with a good algorithm.
> but neither of these bounds seem to be mentioned even in
> passing at the places where I've tried looking for them.
Indeed, the literature says nothing about the complexity of row unification.
I have published a paper about the complexity of solving nonstructural
subtyping constraints that involve rows (in LICS'03).
--
François Pottier
Francois.Pottier at inria.fr
http://pauillac.inria.fr/~fpottier/
More information about the Types-list
mailing list