Two-sided unification is NP-complete

ABSTRACT. It is generally accepted that to unify a pair of substitutions $\theta_1$ and $\theta_2$ means to find out a pair of substitutions $\eta'$ and $\eta''$ such that the compositions $\theta_1\eta'$ and $\theta_2\eta''$ are the same. Actually, unification is the problem of solving linear equations of the form $\theta_1X=\theta_2Y$ in the semigroup of substitutions. But some other linear equations on substitutions may be also viewed as less common variants of unification problem. In this paper we introduce a two-sided unification as the process of bringing a given substitution $\theta_1$ to another given substitution $\theta_2$ from both sides by giving a solution to an equation $X\theta_1Y=\theta_2$. Two-sided unification finds some applications in software refactoring as a means for extracting instances of library subroutines in arbitrary pieces of program code. In this paper we study the complexity of two-sided unification and show that this problem is NP-complete by reducing to it the bounded tiling problem.