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

Задача унификации пары подстановок θ_1 и θ_2 состоит в вычислении такой пары подстановок η' и η'', чтобы композиции θ_1 η' и θ_2 η'' были равны. По существу, задача унификации подстановок равносильна задаче решения линейных уравнений вида θ_1 X=θ_2 Y в полугруппе подстановок. Но некоторые линейные уравнения над подстановками также можно рассматривать как новые варианты задачи унификации. В этой статье мы вводим понятие двусторонней унификации как процесса преобразования одной заданной подстановки θ_1 к другой заданной подстановке θ_2 при помощи композиции, применяемой как справа, так и слева к подстановке θ_1. Иначе говоря, задача двусторонней унификации состоит в решении уравнений вида Xθ_1 Y=θ_2. Двусторонняя унификация подстановок может быть использована при решении одной из задач реорганизации (рефакторинга) программ - выделения в заданном фрагменте кода тела библиотечной процедуры с целью последующей замены выделенного участка кода на вызов этой процедуры. В статье исследован вопрос о сложности задачи двусторонней унификации подстановок. Установлено, что эта задача является NP-полной. Доказательство NP-трудности задачи двусторонней унификации проводится путем сведения к ней NP-полной задачи правильного расположения домино в прямоугольной области плоскости. В статье также сформулирована и исследована задача двусторонней унификации программ в модели программ первого порядка с отношением логико-термальной эквивалентности. Доказано, что сформулированная задача двусторонней унификации программ также является NP-полной.

программа, рефакторинг, логико-термальная эквивалентность, подстановка, композиция, унификация, сложность, проблема домино

1. Захаров В.А., Новикова Т.А. Применение алгебры подстановок для унификации программ // Труды Института системного программирования РАН, - 2011. - т. 21 - с. 141-166.

2. Захаров В.А., Новикова Т.А. Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ. // Труды Института системного программирования РАН, - 2012. - т. 22 - с. 435-455.

3. Захаров В.А., Новикова Т.А. Унификация программ. // Труды Института системного программирования РАН, - 2012. - т. 23 - с. 455-476.

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. - v.4, N 3. - p. 220-249.

7. Котов В.Е., Сабельфельд В.К. Теория схем программ. - М.:Наука, 1991. - 348 с.

8. Иткин В.Э. Логико-термальная эквивалентность схем программ // Кибернетика. - 1972. - N 1. - с. 5-27.

9. Сабельфельд В.К. Полиномиальная оценка сложности распознавания логико-термальной эквивалентности // ДАН СССР. - 1979. - т. 249, N 4. - с. 793-796.

10. Фаулер М. Рефакторинг. Улучшение существующего кода. - Символ-Плюс, 2008. - 432 c.

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. - v. 115.

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

14. Knight K. Unification: a multidisciplinary survey // ACM Computing Surveys - 1989. - v. 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. - v. 16, N 2 - p. 158-167.

17. Martelli A., Montanari U. An efficient unification algorithm //ACM Transactions on Program, Languages and Systems. - 1982. - v. 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 // Jornal of Automated Reasoning. - 1983. - p. 247-283.

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

21. Eder E. Properties of substitutions and unifications // Journal of Symbolic Computations. - v. 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. - v. 2 - N 3. - p. 271-281.

24. Wang Hao. Proving theorems by pattern recognition // Bell System Technical Journal. - 1961. - v. 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. - v.6. - N 1. - p. 88-101.

28. 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].

29. 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].

30. 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].

31. 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.

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

33. 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.

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

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

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

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

38. 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.

39. 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.

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

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

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

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

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

45. 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.

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

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

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

49. 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.

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

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

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

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

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