On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided Distributivity

TL;DR

This paper demonstrates that the Tiden-Arnborg unification algorithm for one-sided distributivity is not polynomial time, providing counterexamples that show it can require exponential steps, challenging previous assumptions.

Contribution

The paper proves the exponential complexity of the Tiden-Arnborg algorithm, contradicting earlier claims of polynomial time bounds.

Findings

Counterexamples show exponential steps in the algorithm

The algorithm's complexity is not polynomial as previously believed

Implications for unification problems in algebraic theories

Abstract

We prove that the Tiden and Arnborg algorithm for equational unification modulo one-sided distributivity is not polynomial time bounded as previously thought. A set of counterexamples is developed that demonstrates that the algorithm goes through exponentially many steps.