A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators
In this paper we study the equivalence problem in the model of sequential programs which assumes that some instructions are commutative and absorbing. Two instructions are commutative if the result of their executions does not depend on an order of their execution. An instruction b absorbs an instru...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/809 |
| _version_ | 1831558313332965376 |
|---|---|
| author | V. V. Podymov V. A. Zakharov |
| author_facet | V. V. Podymov V. A. Zakharov |
| author_sort | V. V. Podymov |
| collection | DOAJ |
| description | In this paper we study the equivalence problem in the model of sequential programs which assumes that some instructions are commutative and absorbing. Two instructions are commutative if the result of their executions does not depend on an order of their execution. An instruction b absorbs an instruction a if the sequential composition a;b yields the same result as the single instruction b. A.A. Letichevskij in 1971 proved the decidability of equivalence checking problem in this model of programs. Nevertheless a possibility of building polynomial time equivalence checking procedures remains an open problem till nowadays. The main result of this paper is the description of a polynomial time algorithm for checking the equivalence of sequential programs with commutative and absorbing instructions. The paper includes 9 sections. In Section 1 we introduce informally the model of programs under consideration, the equivalence checking problem, and give a brief overview of the preceding results in the study of equivalence checking problem for this model. In Sections 2 and 3 the syntax and a semigroup-based semantics of propositional model of sequential programs are formally defined. The algebraic properties of semigroups of commutative and absorbing program instructions are studied in Section 4. In Section 5 we introduce a graph of joined computations which is the key structure in designing our equivalence checking techniques. In Section 6 and 7 we show that the cumulative absorbing effect of finite sequences of commutative instructions can be specified by means of finite automata; this is another key step in building the decision procedure. In Section 8 we show that equivalence checking of two programs is reducible to a traversal of a bounded fragment of the graph of joint computations of these programs; the latter can be performed in time polynomial of the size of programs to be checked. |
| first_indexed | 2024-12-17T05:07:43Z |
| format | Article |
| id | doaj.art-f5120dec7f924c2097c742e5e03a8da5 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-17T05:07:43Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-f5120dec7f924c2097c742e5e03a8da52022-12-21T22:02:22ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0126314516610.15514/ISPRAS-2014-26(3)-8809A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operatorsV. V. Podymov0V. A. Zakharov1Факультет ВМК, МГУ имени М.В. ЛомоносоваИСП РАНIn this paper we study the equivalence problem in the model of sequential programs which assumes that some instructions are commutative and absorbing. Two instructions are commutative if the result of their executions does not depend on an order of their execution. An instruction b absorbs an instruction a if the sequential composition a;b yields the same result as the single instruction b. A.A. Letichevskij in 1971 proved the decidability of equivalence checking problem in this model of programs. Nevertheless a possibility of building polynomial time equivalence checking procedures remains an open problem till nowadays. The main result of this paper is the description of a polynomial time algorithm for checking the equivalence of sequential programs with commutative and absorbing instructions. The paper includes 9 sections. In Section 1 we introduce informally the model of programs under consideration, the equivalence checking problem, and give a brief overview of the preceding results in the study of equivalence checking problem for this model. In Sections 2 and 3 the syntax and a semigroup-based semantics of propositional model of sequential programs are formally defined. The algebraic properties of semigroups of commutative and absorbing program instructions are studied in Section 4. In Section 5 we introduce a graph of joined computations which is the key structure in designing our equivalence checking techniques. In Section 6 and 7 we show that the cumulative absorbing effect of finite sequences of commutative instructions can be specified by means of finite automata; this is another key step in building the decision procedure. In Section 8 we show that equivalence checking of two programs is reducible to a traversal of a bounded fragment of the graph of joint computations of these programs; the latter can be performed in time polynomial of the size of programs to be checked.https://ispranproceedings.elpub.ru/jour/article/view/809программаперестановочные операторыподавляемые операторыэквивалентность программконечный автоматразрешающий алгоритмполиномиальная сложность |
| spellingShingle | V. V. Podymov V. A. Zakharov A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators Труды Института системного программирования РАН программа перестановочные операторы подавляемые операторы эквивалентность программ конечный автомат разрешающий алгоритм полиномиальная сложность |
| title | A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators |
| title_full | A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators |
| title_fullStr | A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators |
| title_full_unstemmed | A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators |
| title_short | A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators |
| title_sort | polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators |
| topic | программа перестановочные операторы подавляемые операторы эквивалентность программ конечный автомат разрешающий алгоритм полиномиальная сложность |
| url | https://ispranproceedings.elpub.ru/jour/article/view/809 |
| work_keys_str_mv | AT vvpodymov apolynomialalgorithmforcheckingtheequivalenceinmodelsofprogramswithcommutationandvastoperators AT vazakharov apolynomialalgorithmforcheckingtheequivalenceinmodelsofprogramswithcommutationandvastoperators AT vvpodymov polynomialalgorithmforcheckingtheequivalenceinmodelsofprogramswithcommutationandvastoperators AT vazakharov polynomialalgorithmforcheckingtheequivalenceinmodelsofprogramswithcommutationandvastoperators |