Двусторонняя унификация программ и ее применение для задач рефакторинга

It is generally accepted that to unify a pair of substitutions θ_1 and θ_2 means to find out a pair of substitutions η' and η'' such that the compositions θ_1 η' and θ_2 η'' are the same. Actually, unification is the problem of solving linear equations of the form θ_1 X=θ_2 Y 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 Xθ_1 Y=θ_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 for substitutions and programs. In Section 1 we discuss the concept of unification on substitutions and programs, outline the recent results on program equivalence checking that involve the concept of unification and anti-unification, and show that the problem of library subroutine extraction may be viewed as the problem of two-sided unification for programs. In Section 2 we formally define the concept of two-sided unification on substitutions and show that the problem of two-unifiability is NP-complete (in contrast to P-completeness of one-sided unifiability problem). NP-hardness of two-sided unifiability problem is established in Section 4 by reducing to it the bounded tiling problem which is known to be NP-complete; the latter problem is formally defined in Section 3. In Section 5 we define two-sided unification of sequential programs in the first-order model of programs supplied with strong equivalence (logic&term equivalence) of programs and proved that this problem is NP-complete. This is the main result of the paper.

program: strong equivalence, substitution, complexity, tiling problem, NP-completeness

1. Zakharov V.A., Novikova T.A. Primininie algebry podstanovok dlya unifikacii program [On the application of substitution algebra to program unification]. Trudy ISP RAN [The Proceedings of ISP RAS], 2011, vol. 21, p. 141-166 [in Russian].

2. Zakharov V.A., Novikova T.A. Polynomialniy po vremeni algoritm proverki logiko-termalnoy ekvivalentnosti program [Polynomial time algorithm for checking strong equivalence of program]. Trudy ISP RAN [The Proceedings of ISP RAS], 2012, vol. 22, p. 435-455 [in Russian].

3. Zakharov V.A., Novikova T.A. Unifikaciya program [Program unification]. Trudy ISP RAN [The Proceedings of ISP RAS], 2012, vol. 23, p. 455-476 [in Russian].

4. Novikova T.A., Zakharov V.A. Is it possible to unify programs? // Proceedings of the 27-th International Workshop on Unification, Epic Series. – 2013. – v. 19 – p. 35-45.

5. Baader F., Snyder W. Unification theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, 2001, v. 1, p. 447-533.

6. Luckham D.C., Park D.M., Paterson M.S. On formalized computer programs // Journal of Computer and System Science. 1970, vol. 4, N 3, p. 220-249.

7. Kotov V.E. Sabelfeld V.K. Teoriya skhem program [Theory of program schemata]. Moscow, “Nauka”, 1991, 348 p.

8. Itkin V.E. Logical-termal equivalence of program schemata. Proceedings of the International Sympoisum on Theoretical Programming, 1972, p. 127-143.

9. Sabelfeld V.K. The Logic-Termal Equivalence is Polynomial-Time Decidable. Information Processing Letters, 1980, vol. 10, N 2, p. 57-62.

10. Fauler M. Refactoring: Improving the design of existing code. 1999, Addison Wesley.

11. Komondoor R., Horwitz S. Using slicing to identify duplication in source code // Proceedings of the 8th International Symposium on Static Analysis. Springer-Verlag, 2001, p. 40–56.

12. Roy C. K., Cordy J. R. A survey on software clone detection research. Technical report TR 2007-541, School of Computing, Queen’s University, 2007, vol. 115.

13. Robinson J.A. A machine-oriented logic based on the resolution principle. Journal of the ACM, 1965, vol. 12, N 1, p. 23-41.

14. Knight K. Unification: a multidisciplinary survey. ACM Computing Surveys. 1989, vol. 21, N 1, p. 93-124.

15. Baxter L.D. An efficient unification algorithm. Technical Report CS-73-23, Dep. of Analysis and Comp. Sci., University of Waterloo, Ontario, Canada, 1973.

16. Paterson M.S., Wegman M.N. Linear unification. The Journal of Computer and System Science. 1978, vol. 16, N 2, p. 158-167.

17. Martelli A., Montanari U. An efficient unification algorithm. ACM Transactions on Program, Languages and Systems. 1982, vol. 4, N 2, p. 258-282.

18. Stickel E.M. A unification algorithm for associative-commutative functions. Journal of the association for Computing Machinary. 1981, v. 28, N 5, p. 423-434.

19. Herold A., Sieckmann J. Unification in Abelean semigroups. Journal of Automated Reasoning. 1983, p. 247-283.

20. Lincoln P., Christian J. Adventures in associative-commutative unification. Journal of Symbolic Computation. 1989, vol. 8, p. 393-416.

21. Eder E. Properties of substitutions and unifications. Journal of Symbolic Computations. vol. 1, 1985, p. 31-46.

22. Lewis C.H. Complexity of solvable cases of the decision problem for predicate calculus. Proceedings of the 19-th Annual Symposium on Foundations of Computer Science, 1978, p. 35-47.

23. Zakharov V.A. On the decidability of the equivalence problem for orthogonal sequential programs. Grammars. 2000, vol. 2, N 3, p. 271-281.

24. Wang Hao. Proving theorems by pattern recognition. Bell System Technical Journal. 1961, vol. 40, N 1, p. 1-41.

25. Berger R. The undecidability of domino problem. Memoirs of American Mathematical Society, v. 66.

26. Lewis C.H., Papadimitriou C.H. Elements of the Theory of Computation – Prentice Hall, Englewood Cliffs, 1981.

27. Itkin V.E., Zwinogrodski Z. On program schemata equivalence. Journal of Computer and System Science. 1972, vol. 6, N 1, p. 88-101.