О задаче минимизации последовательных программ

Стандартные схемы программ — это одна из наиболее простых моделей последовательных императивных программ, предназначенная для решения задач оптимизации и верификации программ. Мы рассматриваем разрешимое отношение логико-термальной эквивалентности стандартных схем программ и задачу минимизации их размера при условии сохранения отношения логико-термальной эквивалентности. Нами доказано, что эта задача является алгоритмически разрешимой. Далее показано, что стандартные схемы программ с отношением логико-термальной эквивалентности и конечные детерминированные автоматы-преобразователи, работающие над полугруппами подстановок, взаимно транслируются друг в друга. Отсюда следует, что также разрешимы задачи проверки эквивалентности и минимизации для преобразователей указанного вида. Кроме того, на основе обнаруженной взаимосвязи выделен подкласс стандартных схем программ, минимизация которых осуществима за полиномиальное время при помощи ранее известных методов минимизации автоматов-преобразователей, работающих над полугруппами. В заключении приведен пример, свидетельствующий о том, что в общем случае задача минимизации автоматов- преобразователей над полугруппой подстановок может иметь несколько неизоморфных решений. 

1. Глушков В. М., Летичевский А. А., “Теория дискретных преобразователей”, Избранные вопросы алгебры и логики, Новосибирск, 1973, 5–39

2. Ершов А. П., “Сведение задачи экономии памяти при составлении программ к задаче раскраски вершин графа”, Доклады АН СССР, 142:4 (1962), 785–787

3. Ершов А. П., “Современное состояние теории схем программ”, Проблемы кибернетики, 27, 1973, 87–110

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

5. Захаров В. А., Подымов В. В., “Применение алгоритмов проверки эквивалентности для оптимизации программ”, Труды Института системного программирования РАН, 27:4 (2015), 145–174

6. Захаров В. А., Темербекова Г. Г., “О минимизации конечных автоматов-преобразователей над полугруппами ”, Моделирование и анализ информационных систем, 23:6 (2016), 741–753

7. Захаров В. А., Проблема эквивалентности программ: модели, алгоритмы, сложность, М., 2016, 304 с.

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

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

10. Криницкий Н. А., Равносильные преобразования алгоритмов и программирование, М., 1970, 304 с.

11. Лавров С. С., “Об экономии памяти в замкнутых операторных схемах”, Журнал вычислительной математики и математической физики, 1:4 (1961), 687–701

12. Ляпунов А. А., “О логических схемах программ”, Проблемы кибернетики, 1, 1958, 46– 74

13. Подловченко Р. И., “Модели последовательных программ, применяемые для изучения функциональной эквивалентности программ”, Кибернетика, 1979, № 1, 20–28

14. Янов Ю. И., “О логических схемах алгоритмов”, Проблемы кибернетики, 1, 1958, 75– 127

15. Eder E., “Properties of substitutions and unifications”, Journal of Symbolic Computations, 1:1 (1985), 31–46.

16. Ershov A. P., “Alpha — an automatic programming system of high efficiency”, Journal of the Association for Computing Machinary, 13:1 (1966), 17–24.

17. Friedman E. P., “Equivalence problems for deterministic languages and monadic recursion schemes”, Journal of Computer System Science, 14:3 (1977), 362–399.

18. Harju T., Karhumaki J., “The equivalence of multi-tape finite automata”, Theoretical Computer Science, 78:2 (1991), 347–355.

19. Luckham D. C., Park D. M., Paterson M. S., “On formalized computer programs”, Journal of Computer and System Science, 4:3 (1970), 220–249.

20. Mohri M., “Minimization algorithms for sequential transducers”, Theoretical Computer Science, 234 (2000), 177–201.

21. Muchnick S., Advanced Compiler Design and Implementation, 1997, 1–856.

22. Rutledge J. D., “Program schemata as automata”, Proc. of the 11-th Annual Symposium on Switching and Automata Theory (SWAT 1970), 1970, 7–24.

23. Sabelfeld V. K., “The logic-termal equivalence is polynomial-time decidable”, Information Processing Letters, 10:2 (1980), 57–62.

24. Senizergues G., “The equivalence problem for deterministic pushdown automata is decidable”, Proc. of the 24-th International Colloquium on Automata, Languages, and Programming (ICALP-1997). Lecture Notes in Computer Science, 1256 (1997), 671–681.

25. Shofrutt C., “Minimizing subsequential transducers: a survey”, Theoretical Computer Science, 292 (2003), 131–143.

26. Watson B.W., “A taxonomy of finite automata minimization algorithm”, Computing Science Report. Eindhoven University of Technology, 93/44 (2005), 1–32.

27. Zakharov V. A., “On the decidability of the equivalence problem for orthogonal sequential programs”, Grammars, 2:3 (1999), 271–281.

28. Zakharov V. A., “Equivalence checking problem for finite state transducers over semigroups”, Proc. of the 6-th International Conference on Algebraic Informatics (CAI- 2015). Lecture Notes in Computer Science, 9270 (2015), 208–221