# On the Minimization Problem for Sequential Programs

## Abstract

First-order program schemata represent one of the most simple models of sequential imperative programs intended for solving verification and optimization problems. We consider the decidable relation of logical-thermal equivalence on 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 makes it possible to adapt equivalence checking and minimization algorithms developed in one of these models of computation to the solution of the same problems for the other model of computation. In addition, on the basis of the discovered relationship, we describe a subclass of first-order program schemata such that minimization of the program schemata from this class 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 the general case the minimization problem for finite state transducers over semigroups may have several non-isomorphic solutions.

## Keywords

sequential program transducer minimization substitution semigroup equivalence## Preview

Unable to display preview. Download preview PDF.

## References

- 1.Glushkov, V.M. and Letichevsky, A.A., Theory of discrete transducers,
*Vopr. Algebry Logiki*, 1973, pp. 5–39Google Scholar - 2.Ershov, A.P., Reducing the problem of saving memory when making programs to the problem of graph vertex coloring,
*Dokl. Akad. Nauk SSSR*, 1962, vol. 142, no. 4, pp. 785–787.MathSciNetGoogle Scholar - 3.Ershov, A.P., Current state of the theory of program schemes,
*Probl. Kibern.*, 1973, vol. 27, pp. 87–110.Google Scholar - 4.Zakharov, V.A. and Novikiva, T.A., A time-polynomial algorithm for verifying the logical-thermal equivalence of programs,
*Tr. Inst. Sist. Progr.*, 2012, vol. 22, no. 4, pp. 435–455.Google Scholar - 5.Zakharov, V.A. and Podymov, V.V., Application of equivalence checking algorithms for program optimization,
*Tr. Inst. Sist. Progr.*, 2015, vol. 27, no. 3, pp. 145–174.Google Scholar - 6.Zakharov, V.A. and Temerbekova, G.G., On the minimization and equivalence checking of sequential reactive systems,
*Syst. Inf.*, 2016, vol. 7, pp. 33–44.Google Scholar - 7.Zakharov, V.A.,
*Problemy ekvivalentnosti program: Modeli, algoritmy, slojnost*(Program Equivalence Problems: Models, Algorithms, and Complexity), 2016, pp. 1–304Google Scholar - 8.Itkin, V.E., Logical-thermal equivalence of programs,
*Kibernetika*, 1972, no. 1, pp. 5–27.Google Scholar - 9.Kotov, V.E. and Sabelfeld, V.K.,
*Teoriya skhem program*(Theory of Program Schemes), 1991, pp. 1–348Google Scholar - 10.Krinickij, N.A.,
*Ravnosil’nye preobrazovaniya algoritmov i programmirovanie*(Equivalent Algorithm Transformations and Programming), 1970, pp. 1–210Google Scholar - 11.Lavrov, S.S., About saving memory in closed operator schemes,
*Zh. Vychisl. Mat. Mat. Fiz.*, 1961, vol. 1, no. 4, pp. 15–19.Google Scholar - 12.Lyapunov, A.A., About logical schemes of programs,
*Probl. Kibern.*, 1958, vol. 1, pp. 46–74.Google Scholar - 13.Podlovchenko, R.I., Models of sequential programs used to study the functional equivalence of programs,
*Kibernetika*, 1979, no. 1, pp. 20–28.MathSciNetMATHGoogle Scholar - 14.Yanov, Yu.I., On logical schemes of algorithms,
*Probl. Kibern.*, 1958, vol. 1, pp. 75–127.MathSciNetMATHGoogle Scholar - 15.Eder, E., Properties of substitutions and unifications,
*J. Symbolic Comput.*, 1985, vol. 1, no. 1, pp. 31–46.MathSciNetCrossRefMATHGoogle Scholar - 16.Ershov, A.P., Alpha—an automatic programming system of high efficiency,
*J. Assoc. Comput. Mach.*, 1966, vol. 13, no. 1, pp. 17–24.CrossRefGoogle Scholar - 17.Friedman, E.P., Equivalence problems for deterministic languages and monadic recursion schemes,
*J. Comput. Syst. Sci.*, 1977, vol. 14, no. 3, pp. 362–399.MathSciNetCrossRefGoogle Scholar - 18.Harju, T. and Karhumaki, J., The equivalence of multi-tape finite automata,
*Theor. Comput. Sci.*, 1991, vol. 78, no. 2, pp. 347–355.CrossRefMATHGoogle Scholar - 19.Luckham, D.C., Park, D.M., and Paterson, M.S., On formalized computer programs,
*J. Comput. Syst. Sci.*, 1970, vol. 4, no. 3, pp. 220–249.CrossRefMATHGoogle Scholar - 20.Mohri, M., Minimization algorithms for sequential transducers,
*Theor. Comput. Sci.*, 2000, vol. 234, pp. 177–201.MathSciNetCrossRefMATHGoogle Scholar - 21.Muchnick, S.,
*Advanced Compiler Design and Implementation*, 1997, pp. 1–856Google Scholar - 22.Rutledge, J.D., Program schemata as automata,
*Proc. of the 11-th Annual Symposium on Switching and Automata Theory (SWAT 1970)*, 1970, pp. 7–24CrossRefGoogle Scholar - 23.Sabelfeld, V.K., The logic-termal equivalence is polynomial-time decidable,
*Inf. Process. Lett.*, 1980, vol. 10, no. 2, pp. 57–62.MathSciNetCrossRefMATHGoogle Scholar - 24.Senizergues, G., The equivalence problem for deterministic pushdown automata is decidable,
*Lect. Notes Comput. Sci.*, 1997, vol. 1256, pp. 271–281.MathSciNetGoogle Scholar - 25.Shofrutt, C., Minimizing subsequential transducers: A survey,
*Theor. Comput. Sci.*, 2003, vol. 292, pp. 131–143.MathSciNetCrossRefMATHGoogle Scholar - 26.Watson, B.W., A taxonomy of finite automata minimization algorithm,
*Comput. Sci. Rep., Eindhoven Univ. Technol.*, 2005, vol. 93, no. 44, pp. 1–32.Google Scholar - 27.Zakharov, V.A., On the decidability of the equivalence problem for orthogonal sequential programs,
*Grammars*, 1999, vol. 2, no. 3, pp. 271–281.MathSciNetCrossRefMATHGoogle Scholar - 28.Zakharov, V.A., Equivalence checking problem for finite state transducers over semigroups,
*Lect. Notes Comput. Sci.*, 2015, vol. 9270, pp. 208–221.MathSciNetCrossRefMATHGoogle Scholar