maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2017-4-415-433mais-532Research ArticleОригинальные статьиArticlesО задаче минимизации последовательных программOn the Minimization Problem for Sequential Programshttps://orcid.org/0000-0002-3794-9565ЗахаровВладимир АнатольевичZakharovVladimir A.

д-р физ.-мат. наук, ст. науч. сотр., факультет компьютерных наук

PhD, senior researcher, Faculty of Computer Science

zakh@cs.msu.ruЖайлауоваШынар РустамбековнаZhailauovaShynar R.

магистр, факультет ВМК

graduate student, Faculty of Computational Mathematics and Cybernetics

gulgaisha93@mail.ruНациональный исследовательский университет "Высшая школа экономики"РоссияNational Reserach University Higher School of EconomicsRussian FederationМосковский государственный университет им. М.В. ЛомоносоваРоссияLomonosov Moscow State UniversityRussian Federation201731082017244415433Copyright © Захаров В.А., Жайлауова Ш.Р., 20172017Захаров В.А., Жайлауова Ш.Р.Zakharov V.A., Zhailauova S.R.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/532

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

First-order program schemata is one of the simplest models of sequential imperative programs intended for solving verification and optimization problems. We consider the decidable relation of logical-thermal equivalence of these schemata and the problem of their size minimization while preserving logical-thermal equivalence. We prove that this problem is decidable. Further we show that the first-order program schemata supplied with logical-thermal equivalence and finite state deterministic transducers operating over substitutions are mutually translated into each other. This relationship implies that the equivalence checking problem and the minimization problem for these transducers are also decidable. In addition, on the basis of the discovered relationship, we have found a subclass of firstorder program schemata such that their minimization can be performed in polynomial time by means of known techniques for minimization of finite state transducers operating over semigroups. Finally, we demonstrate that in general case the minimization problem for finite state transducers over semigroups may have several non-isomorphic solutions.

последовательная программаавтомат-преобразовательминимизацияподстановкаполугруппаэквивалентностьsequential programtransducerminimizationsubstitutionsemigroupequivalenceReferencesГлушков В. М., Летичевский А. А., “Теория дискретных преобразователей”, Избранные вопросы алгебры и логики, Новосибирск, 1973, 5–39Glushkov V. M., Letichevskij A. A., “Teoriya diskretnyh preobrazovatelej”, Izbrannye voprosy algebry i logiki, Novosibirsk, 1973, 5–39, (in Russian)Ершов А. П., “Сведение задачи экономии памяти при составлении программ к задаче раскраски вершин графа”, Доклады АН СССР, 142:4 (1962), 785–787Ershov A. P., “Svedenie zadachi ekonomii pamyati pri sostavlenii programm k zadache raskraski vershin grafa”, Doklady AN SSSR, 142:4 (1962), 785–787, (in Russian)Ершов А. П., “Современное состояние теории схем программ”, Проблемы кибернетики, 27, 1973, 87–110Ershov A. P., “Sovremennoe sostoyanie teorii skhem program”, Problemy kibernetiki, 27 (1973), 87–110, (in Russian)Захаров В. А., Новикова Т. А., “Полиномиальный по времени алгоритм проверки логико-термальной эквивалентности программ ”, Труды Института системного программирования РАН, 22 (2012), 435–455Zakharov V. A., Novikova T. A., “Polynomial time algorithm for checking strong equivalence of program”, Proceedings of the Institute for System Programming, 22 (2012), 435–455, (in Russian)Захаров В. А., Подымов В. В., “Применение алгоритмов проверки эквивалентности для оптимизации программ”, Труды Института системного программирования РАН, 27:4 (2015), 145–174Zakharov V. A., Podymov V. V., “On the application of equivalence checking algorithms for program minimization”, Proceedings of the Institute for System Programming, 27:4 (2015), 145–174, (in Russian)Захаров В. А., Темербекова Г. Г., “О минимизации конечных автоматов-преобразователей над полугруппами ”, Моделирование и анализ информационных систем, 23:6 (2016), 741–753Zakharov V. A., Temerbekova G. G., “On the Minimization of Finite State Transducers over Semigroups”, Modeling and Analysis of Information Systems, 23:6 (2016), 741–753, (in Russian)Захаров В. А., Проблема эквивалентности программ: модели, алгоритмы, сложность, М., 2016, 304 с.Zakharov V. A., Problema ekvivalentnosti programm: modeli, algoritmy, slozhnost, Moskva, 2016, 304 pp., (in Russian)Иткин В. Э., “Логико-термальная эквивалентность схем программ”, Кибернетика, 1972, № 1, 5–27Itkin V. E., “Logiko-termalnaya ekvivalentnost skhem program”, Cybernetics, 1972, № 1, 5–27, (in Russian)Котов В. Е., Сабельфельд В. К., Теория схем программ, Наука, М., 1991, 248 с.Kotov V. E., Sabel’fel’d V. K., Teoriya skhem program, Nauka, Moskva, 1991, 248 pp., (in Russian)Криницкий Н. А., Равносильные преобразования алгоритмов и программирование, М., 1970, 304 с.Krinitskiy N. A., Ravnosilnye preobrazovaniya algoritmov i programmirovanie, Moskva, 1970, 304 pp., (in Russian)Лавров С. С., “Об экономии памяти в замкнутых операторных схемах”, Журнал вычислительной математики и математической физики, 1:4 (1961), 687–701Lavrov S. S., “Store economy in closed operator schemes”, U.S.S.R. Comput. Math. Math. Phys., 1:3 (1962), 810–828Ляпунов А. А., “О логических схемах программ”, Проблемы кибернетики, 1, 1958, 46– 74Lyapunov A. A., “O logicheskikh skhemakh program”, Problemy kibernetiki, 1, 1958, 46–74, (in Russian)Подловченко Р. И., “Модели последовательных программ, применяемые для изучения функциональной эквивалентности программ”, Кибернетика, 1979, № 1, 20–28Podlovchenko R. I., “Models of sequential programs used to study functional equivalence of programs”, Cybern Syst Anal, 15:1 (1979), 22–31.Янов Ю. И., “О логических схемах алгоритмов”, Проблемы кибернетики, 1, 1958, 75– 127Yanov Yu. I., “O logicheskikh skhemakh algoritmov”, Problemy kibernetiki, 1, 1958, 75–127, (in Russian)Eder E., “Properties of substitutions and unifications”, Journal of Symbolic Computations, 1:1 (1985), 31–46.Eder E., “Properties of substitutions and unifications”, Journal of Symbolic Computations, 1:1 (1985), 31–46Ershov A. P., “Alpha — an automatic programming system of high efficiency”, Journal of the Association for Computing Machinary, 13:1 (1966), 17–24.Ershov A. P., “Alpha — an automatic programming system of high efficiency”, Journal of the Association for Computing Machinary, 13:1 (1966), 17–24.Friedman E. P., “Equivalence problems for deterministic languages and monadic recursion schemes”, Journal of Computer System Science, 14:3 (1977), 362–399.Friedman E. P., “Equivalence problems for deterministic languages and monadic recursion schemes”, Journal of Computer System Science, 14:3 (1977), 362–399.Harju T., Karhumaki J., “The equivalence of multi-tape finite automata”, Theoretical Computer Science, 78:2 (1991), 347–355.Harju T., Karhumaki J., “The equivalence of multi-tape finite automata”, Theoretical Computer Science, 78:2 (1991), 347–355.Luckham D. C., Park D. M., Paterson M. S., “On formalized computer programs”, Journal of Computer and System Science, 4:3 (1970), 220–249.Luckham D. C., Park D. M., Paterson M. S., “On formalized computer programs”, Journal of Computer and System Science, 4:3 (1970), 220–249.Mohri M., “Minimization algorithms for sequential transducers”, Theoretical Computer Science, 234 (2000), 177–201.Mohri M., “Minimization algorithms for sequential transducers”, Theoretical Computer Science, 234 (2000), 177–201.Muchnick S., Advanced Compiler Design and Implementation, 1997, 1–856.Muchnick S., Advanced Compiler Design and Implementation, 1997, 1–856.Rutledge J. D., “Program schemata as automata”, Proc. of the 11-th Annual Symposium on Switching and Automata Theory (SWAT 1970), 1970, 7–24.Rutledge J. D., “Program schemata as automata”, Proc. of the 11-th Annual Symposium on Switching and Automata Theory (SWAT 1970), 1970, 7–24.Sabelfeld V. K., “The logic-termal equivalence is polynomial-time decidable”, Information Processing Letters, 10:2 (1980), 57–62.Sabelfeld V. K., “The logic-termal equivalence is polynomial-time decidable”, Information Processing Letters, 10:2 (1980), 57–62.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.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.Shofrutt C., “Minimizing subsequential transducers: a survey”, Theoretical Computer Science, 292 (2003), 131–143.Shofrutt C., “Minimizing subsequential transducers: a survey”, Theoretical Computer Science, 292 (2003), 131–143.Watson B.W., “A taxonomy of finite automata minimization algorithm”, Computing Science Report. Eindhoven University of Technology, 93/44 (2005), 1–32.Watson B.W., “A taxonomy of finite automata minimization algorithm”, Computing Science Report. Eindhoven University of Technology, 93/44 (2005), 1–32.Zakharov V. A., “On the decidability of the equivalence problem for orthogonal sequential programs”, Grammars, 2:3 (1999), 271–281.Zakharov V. A., “On the decidability of the equivalence problem for orthogonal sequential programs”, Grammars, 2:3 (1999), 271–281.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–221Zakharov 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.

The authors declare that there are no conflicts of interest present.