Полиномиальный алгоритм проверки эквивалентности в модели программ с перестановочными и подавляемыми операторами

В статье исследована задача проверки эквивалентности последовательных программ, некоторые операторы которых обладают свойствами перестановочности и подавления. Два оператора считаются перестановочными, если результат их последовательного выполнения не зависит от порядка, в котором эти операторы выполняются. Считается, что оператор b подавляет оператор a , если последовательное выполнение операторов a и b дает такой же результат, что и выполнение одного лишь оператора b . Разрешимость проблемы эквивалентности в исследуемой модели программ была установлена в 1971 г. А.А. Летичевским. Однако с тех пор вопрос о сложности проверки эквивалентности таких программ оставался открытым. Основной результат статьи - алгоритм, осуществляющий проверку эквивалентности программ с перестановочными и подавляемыми операторами за время, полиномиально зависящее от размеров анализируемых программ.

программа, перестановочные операторы, подавляемые операторы, эквивалентность программ, конечный автомат, разрешающий алгоритм, полиномиальная сложность

1. Ахо А., Лам М., Сети Р., Ульман Д. Компиляторы: принципы, технологии и инструментарий. - 2-е издание. - М.: «Вильямс», 2008. - 1184 с.

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

3. Ершов А.П. Сведение задачи экономии памяти при составлении программ к задаче раскраски вершин графа // Доклады АН СССР. - 1962. - т. 142, N 4. - с. 785-787.

4. Глушков В.М. Теория автоматов и формальные преобразования микропрограмм // Кибернетика. - 1965. - N 5. - c. 1-9.

5. Ляпунов А.А. О логических схемах программ // Проблемы кибернетики, вып. 1. - М.:Физматгиз, 1958. - с. 46-74.

6. Янов Ю.И. О логических схемах алгоритмов // Проблемы кибернетики, вып. 1. - М.:Физматгиз, 1958. - с. 75-127.

7. Ершов А.П. Операторные схемы (Об операторных схемах Янова) // Проблемы кибернетики, вып. 20. - М.:Физматгиз, 1967. - с. 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. Глушков В.М., Летичевский А.А. Теория дискретных преобразователей. // Избранные вопросы алгебры и логики: сб.статей. - Новосибирск: Наука, 1973. - с. 5-39.

10. Ершов А.П. Современное состояние теории схем программ // Проблемы кибернетики, вып. 27. - М.:Наука, 1973. - с. 87-110.

11. Подловченко Р.И., Захаров В.А. Полиномиальный по сложности алгоритм, распознающий коммутативную эквивалентность схем программ // Доклады РАН, серия Информатика. - 1998. - т. 362, N 6. - с. 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. Захаров В.А. Быстрые алгоритмы разрешения эквивалентности операторных программ на уравновешенных шкалах // Математические вопросы кибернетики, вып.7. - М.:Физматлит, 1998. - c. 303-324.

14. Захаров В.А. Проверка эквивалентности программ при помощи двухленточных автоматов // Кибернетика и системный анализ. - 2010. - N 4. - c. 39-48.

15. Захаров В.А., Щербина В.Л. Об эквивалентности программ с операторами, обладающими свойствами коммутативности и подавления // Материалы 9-го Международного семинара «Дискретная математика и ее приложения», Москва, 2007. - 2007. - c. 191-194.

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

17. Подымов В.В., Захаров В.А. Об одной полугрупповой модели программ, определяемой при помощи двухленточных автоматов // Научные ведомости Белгородского государственного университета. Серия История, экономика, политология, информатика, том 14. - № 7. - с. 94-101.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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