Polynomial time algorithm for checking strong equivalence of program
Abstract
Strong (logic&term) equivalence of programs is the weakest decidable equivalence relation which approximates the functional equivalence of programs. In this paper we develop a new variant of the algorithm for checking strong equivalence of programs. A distinguished feature of our algorithm is that it relies completely on the algebra of finite substitutions which includes the operations of composition and antiunification. The paper begins with a short introduction to the theory of first-order substitutions. In the next section the formal first-order model of sequential programs and strong equivalence are defined. We also describe a preliminary variant of equivalence checking algorithm. This algorithm deals with composition and antiunification operations on finite substitutions. Since the complexity of these operations depends on data structures that represent substitutions, we consider in Section 4 graph-theoretic representations of substitutions as well as upper and lower bounds on the complexity of basic operations on substitutions. To reduce the complexity of equivalence checking algorithm for sequential programs we introduce in Section 5 a new class of truncated substitutions and study the basic algebraic properties of composition and antiunification operations on truncated substitutions. In Section 6 we showed that both operations on truncated substitutions can be performed in time O(n^2). Finally, in Section 7 using the properties of truncated substitutions we introduced an improved version of the equivalence checking algorithm and proved that its time complexity is O(n^6) on the size of programs to be checked.
About the Authors
V. A. Zakharov
ISP RAS
Russian Federation
Russian Federation
T. A. Novikova
Kazakhstan Branch of Lomonosov Moscow State University
Kazakhstan
Kazakhstan
References
1. Itkin V.E. Logical-termal equivalence of program schemata. Proceedings of the International Sympoisum on Theoretical Programming, 1972, p. 127-143.
2. Sabel'fel'd V.K. Polinomial'naja ocenka slozhnosti raspoznavanija logiko-termal'noj jekvivalentnosti [Polynomial time algorithm for checking strong equivalence of program] DAN SSSR [Reports of USSR Academy of Science], 1979, t. 249, N 4, s. 793-796 [in Russian].
3. Sabelfeld V.K. The logic-termal equivalence is polynomial-time decidable. Information Processing Letters, 1980, v. 10, N 2, p. 57-62.
4. Buda A.O., Itkin V.E. Svodimost’ ekvivalentnosti program k termal’noy ekvivalentnosti [On the reducibility of program equivalence to termal equivalence]. Sistemnoye I teoreticheskoye programirovaniye [Proceeding of the conference on System and Theoretic Programming], vol. 1, Cisinau, 1974, p. 293-324 [in Russian].
5. Buda A.O. Ob odnoy modeli vychisleniy nad pamat’yu s razreshimoy problemoy ekvivalentnosti [On a random access memory model of computation with decidable equivalence checking problem]. Doklady Akademii Nauk [Reports of USSR Academy of Science], 1979, vol. 245, no 1 [in Russian].
6. Buda A.O. Kanonizaciaya logicheskoy struktuty logiko-termal’no ekvivalentnyh shem program [On canonization of logical structure of logic-termal equivalent program schemata]. Translaciya i Modeli program [Translation and program models], Novosibirsk, 1980 [in Russian].
7. Godlevsky A.B. O svyazi logiko-termal’noy ekvivalentnosti shem program s odnim sluchaem special’noy problem ekvivalentnosti diskrenyh preobrazovateley [On the relationship of logic-termal equivalence of program schemata with some special case of equivalence problem for discrete transducers]. Cybernetics, 1975, N 5, p. 32-34 [in Russian].
8. Khachatryan V.Y. Logiko-termal’naya ekvivalentost’ v klasse shem nad sil’no nevyrizhdennym bazisom [Logic-termal equivalence in a class of schemata over strongly nondegenerated basis]. Programirovaniye [Programming and Computer Software], 1977, N 3, p. 20-27 [in Russian].
9. Sabelfeld V.K. Nekotoriye optomiziruyushchiye preobrazovaniya dly standartnyh shem program [Some optimization transformations for standard program schemata]. Yazyki i sistemy programirovaniya [Languages and programming systems]. Novosibirsk, 1979 [in Russian].
10. Sin Min De. Logiko-termal’niye probrazovaniya shem program [Logic-termal transformations of program schemata]. Kibernetika [Cybernetics], 1976, N 5 [in Russian].
11. Fauler M. Refactoring: Improving the design of existing code. 1999, Addison Wesley.
12. 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.
13. Bulychev P., Kostylev E., Zakharov V. Anti-unification algorithms and their applications in program analysis // Proceedings of the 7th International Conference “Perspectives of System Informatics”, June 15-19, 2009, Novosibirsk, 2009, p. 82-89.
14. 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.
15. Itkin V.E., Zwinogrodski Z. On program schemata equivalence. Journal of Computer and System Science, 1972, v. 6, N 1, p. 88-101.
16. Kotov V.E. Sabelfeld V.K. Teoriya skhem program [Theory of program schemata]. Moscow, “Nauka”, 1991, 348 p.
17. Eder E. Properties of substitutions and unifications. Journal of Symbolic Computations, v. 1, 1985, p. 31-46.
18. Palamidessi C. Algebraic properties of idempotent substitutions. Lecture Notes in Computer Science, v. 443, 1990, p. 386-399.
19. Plotkin G.D. A note on inductive generalization. Machine Intelligence, 1970, v. 5, N 1, p. 153-163.
20. Sorensen M. H., Gluck. R. An algorithm of generalization in positive supercompilation. Proceedings of the 1995 International Symposium on Logic Programming._MIT Press, 1995, p. 465-479.
21. Zakharov V.A., Kostylev E.V. On the complexity of anti-unification. Discrete Mathematics, 2008, vol. 20, N 1, p. 131-144.
22. Zakharov V.A. On the refinement of logic programs by means of anti-unification. Proceedings of the 2nd Panhellenic Logic Symposium, Delphi, Greece, 1999, p. 219-224.
23. 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].
Review
For citations:
Zakharov V.A., Novikova T.A. Polynomial time algorithm for checking strong equivalence of program. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2012;22. (In Russ.)
Email this article 