• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Book chapter

Two-sided unification is NP-complete

P. 55-61.
Zakharov V., Новикова Т. А.
It is generally accepted that to unify a pair of substitutions 1 and 2 means to find out a pair of substitutions 0 and 00 such that the compositions 10 and 200 are the same. Actually, unification is the problem of solving linear equations of the form 1X = 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 1 to another given substitution 2 from both sides by giving a solution to an equation X1Y = 2. Twosided 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.

In book

Linz: Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, 2014.