On the Minimization Problem for Sequential Programs
https://doi.org/10.18255/1818-1015-2017-4-415-433
Abstract
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.
About the Authors
Vladimir A. Zakharov
National Reserach University Higher School of Economics
Russian Federation
PhD, senior researcher, Faculty of Computer Science
Russian Federation
PhD, senior researcher, Faculty of Computer Science
Shynar R. Zhailauova
Lomonosov Moscow State University
Russian Federation
graduate student, Faculty of Computational Mathematics and Cybernetics
Russian Federation
graduate student, Faculty of Computational Mathematics and Cybernetics
References
1. Glushkov V. M., Letichevskij A. A., “Teoriya diskretnyh preobrazovatelej”, Izbrannye voprosy algebry i logiki, Novosibirsk, 1973, 5–39, (in Russian)
2. Ershov A. P., “Svedenie zadachi ekonomii pamyati pri sostavlenii programm k zadache raskraski vershin grafa”, Doklady AN SSSR, 142:4 (1962), 785–787, (in Russian)
3. Ershov A. P., “Sovremennoe sostoyanie teorii skhem program”, Problemy kibernetiki, 27 (1973), 87–110, (in Russian)
4. Zakharov 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)
5. Zakharov 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)
6. Zakharov 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)
7. Zakharov V. A., Problema ekvivalentnosti programm: modeli, algoritmy, slozhnost, Moskva, 2016, 304 pp., (in Russian)
8. Itkin V. E., “Logiko-termalnaya ekvivalentnost skhem program”, Cybernetics, 1972, № 1, 5–27, (in Russian)
9. Kotov V. E., Sabel’fel’d V. K., Teoriya skhem program, Nauka, Moskva, 1991, 248 pp., (in Russian)
10. Krinitskiy N. A., Ravnosilnye preobrazovaniya algoritmov i programmirovanie, Moskva, 1970, 304 pp., (in Russian)
11. Lavrov S. S., “Store economy in closed operator schemes”, U.S.S.R. Comput. Math. Math. Phys., 1:3 (1962), 810–828
12. Lyapunov A. A., “O logicheskikh skhemakh program”, Problemy kibernetiki, 1, 1958, 46–74, (in Russian)
13. Podlovchenko R. I., “Models of sequential programs used to study functional equivalence of programs”, Cybern Syst Anal, 15:1 (1979), 22–31.
14. Yanov Yu. I., “O logicheskikh skhemakh algoritmov”, Problemy kibernetiki, 1, 1958, 75–127, (in Russian)
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.
Review
For citations:
Zakharov V.A., Zhailauova Sh.R. On the Minimization Problem for Sequential Programs. Modeling and Analysis of Information Systems. 2017;24(4):415-433. (In Russ.) https://doi.org/10.18255/1818-1015-2017-4-415-433
Views:
1020
Email this article 