A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators

In this paper we study the equivalence problem in the model of sequential programs which assumes that some instructions are commutative and absorbing. Two instructions are commutative if the result of their executions does not depend on an order of their execution. An instruction b absorbs an instruction a if the sequential composition a;b yields the same result as the single instruction b. A.A. Letichevskij in 1971 proved the decidability of equivalence checking problem in this model of programs. Nevertheless a possibility of building polynomial time equivalence checking procedures remains an open problem till nowadays. The main result of this paper is the description of a polynomial time algorithm for checking the equivalence of sequential programs with commutative and absorbing instructions. The paper includes 9 sections. In Section 1 we introduce informally the model of programs under consideration, the equivalence checking problem, and give a brief overview of the preceding results in the study of equivalence checking problem for this model. In Sections 2 and 3 the syntax and a semigroup-based semantics of propositional model of sequential programs are formally defined. The algebraic properties of semigroups of commutative and absorbing program instructions are studied in Section 4. In Section 5 we introduce a graph of joined computations which is the key structure in designing our equivalence checking techniques. In Section 6 and 7 we show that the cumulative absorbing effect of finite sequences of commutative instructions can be specified by means of finite automata; this is another key step in building the decision procedure. In Section 8 we show that equivalence checking of two programs is reducible to a traversal of a bounded fragment of the graph of joint computations of these programs; the latter can be performed in time polynomial of the size of programs to be checked.

program, commuting instructions, absorbing instructions, program equivalence, finite automata, decision procedure, polynomial time complexity

1. Aho A., Lam M., Sethi R, Ullman J. D. Compilers: Principles, Techniques, and Tools. Pearson Education, Ltd., 2014, 940 p.

2. Hoare C.A.R. An axiomatic basis for computer programming. Communications of the ACM. 1969, v. 12, N 10, p. 576-580.

3. Ershov, A. P. Axiomatics for Memory Allocation, Acta Inform., Vol. 6, 1976, pp. 61-75.

4. Glushkov V.M. Teoriya avtomatov i formalnyie preobrazovaniya mikroprogramm [Automata theory and formal transformations of microprograms]. Kybernetika [Cybernetics], 1965, N 5.

5. Lyapunov A.A. O logicheskih shemah programm [On the logical program schemata]. Problemy kibernetiki [Problems of cybernetics], 1958, vol. 1, p. 46-74.

6. Yanov Ju. I. O logicheskih shemah algoritmov [On the logical algorithm schemata]. Problemy kibernetiki [Problems of cybernetics], 1958, vol. 1, p. 75-127.

7. Ershov A.P. Operatornye skhemy (Ob operatornykh skhemakh Yanova) [Operating schemata (On Yanov operator shemata)]. Problemy kibernetiki [Problems of cybernetics], 1967, v. 20, p. 181-200.

8. Ershov A.P. Alpha – an automatic programming system of high efficiency // Journal of the Association for Computing Machinary. – 1966. – v. 13, N 1. – p. 17-24.

9. Glushkov V.M., Letichevsky A.A. Teoriya diskretnykh preobrazovateley [Theory of discrete transducers]. Izbrannye voprosy algebry i logiki: sb.statey.. Izbrannyje voprosy algebry I logiki [Selected problems in algebra and logics: Proceedings], 1973, Novosibirsk: Nauka, p. 5-39.

10. Ershov, A. P., Theory of Program Schemata. Proc. IFIP 1971, North-Holland, Amsterdam, pp. 144-163.

11. Podlovchenko R.I., Zakharov V.A. Polinomial’niy po slojnosti algoritm raspoznayushchiy ekvivalentost skhem program [Polynomial equivalence checking algorithm for program schemata], Doklady Mathematics (Doklady Akademii Nauk), 1998, vol. 362, N 6, p. 27-31.

12. Zakharov V.A. An efficient and unified approach to the decidability of equivalence of propositional program schemes. Lecture Notes in Computer Science, 1998, v. 1443, p. 247-258.

13. Zakharov V.A. Byistryie algoritmyi razresheniya ekvivalentnosti operatornyih programm na uravnoveshennyih shkalah [Swift algorithms deciding equivalence of operator schemata on length-preserving frames]. Matematicheskie voprosyi kibernetiki [Mathematical Problems of Cybernetics], vol.7. – Moscow PhysMathLit, 1998, p. 303-324.

14. Zakharov V.A. Program equivalence checking by two-tape automata. Cybernetics and Systems Analysis. 46, № 4, p. 554-562.

15. Zakharov V.A., Shcherbina V.L. Ob ekvivalentnosti programm s operatorami, obladayushchimi svoystvami kommutativnosti i podavleniya [On the equivalence of programs with commutative and absorbing operators]. Materialy 9-go Mezhdunarodnogo seminara «Diskretnaya matematika i eye prilozheniya» [Proceedings of the 9-th International Workshop “Discrete mathematics and its application”], Mosocw, 2007, p. 191-194.

16. Harel D., Kozen D., Tiuryn J. Dynamic logic. MIT Press, Cambridge, MA, USA. – 2000. – 450 p.

17. Podymov V.V., Zakharov V.A. Ob odnoy polugruppovoy modeli programm, opredelyaemoy pri pomoshchi dvukhlentochnykh avtomatov [On a semigroup model of programs specified by two-tape automata]. Nauchnye vedomosti Belgorodskogo gosudarstvennogo universiteta. Seriya Istoriya, ekonomika, politologiya, informatika [Scientific Bulletin of Belgorod State University: History, Economics, Politology, Informatics], vol 14. N 7, p. 94-101.

18.