On the minimization problem for sequential programs

V. A. Zakharov ; Sh. R. Zhailauova

Modelirovanie i analiz informacionnyh sistem, Tome 24 (2017) no. 4, pp. 415-433.

Résumé

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 first-order 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.

Détail

Keywords: sequential program, transducer, minimization, semigroup
Mots-clés : substitution, equivalence.

Bibliographie

[1] Glushkov V. M., Letichevskij A. A., “Teoriya diskretnyh preobrazovatelej”, Izbrannye voprosy algebry i logiki, Novosibirsk, 1973, 5–39 (in Russian) | Zbl

[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) | Zbl

[3] Ershov A. P., “Sovremennoe sostoyanie teorii skhem program”, Problemy kibernetiki, 27, 1973, 87–110 (in Russian) | MR | Zbl

[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) | MR

[7] Zakharov V. A., Problema ekvivalentnosti programm: modeli, algoritmy, slozhnost, M., 2016, 304 pp. (in Russian)

[8] Itkin V. E., “Logiko-termalnaya ekvivalentnost skhem program”, Cybernetics, 1972, no. 1, 5–27 (in Russian) | MR | Zbl

[9] Kotov V. E., Sabel'fel'd V. K., Teoriya skhem program, Nauka, M., 1991, 248 pp. (in Russian) | MR

[10] Krinitskiy N. A., Ravnosilnye preobrazovaniya algoritmov i programmirovanie, M., 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 | DOI | MR | Zbl

[12] Lyapunov A. A., “O logicheskikh skhemakh program”, Problemy kibernetiki, 1, 1958, 46–74 (in Russian) | MR | Zbl

[13] Podlovchenko R. I., “Models of sequential programs used to study functional equivalence of programs”, Cybern. Syst. Anal., 15:1 (1979), 22–31 | DOI | MR | Zbl

[14] Yanov Yu. I., “O logicheskikh skhemakh algoritmov”, Problemy kibernetiki, 1, 1958, 75–127 (in Russian) | Zbl

[15] Eder E., “Properties of substitutions and unifications”, Journal of Symbolic Computations, 1:1 (1985), 31–46 | DOI | MR | Zbl

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

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

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

[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 | DOI | MR | Zbl

[20] Mohri M., “Minimization algorithms for sequential transducers”, Theoretical Computer Science, 234 (2000), 177–201 | DOI | MR | Zbl

[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 | DOI | MR | Zbl

[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 | DOI | MR

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

[26] Watson B. W., A taxonomy of finite automata minimization algorithm, Computing Science Report No 93/44, Eindhoven University of Technology, 2005, 32 pp.

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

[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 | DOI | MR | Zbl