Ivannikov Institute for System Programming of the RAS

Is it possible to unify sequential programs.


Novikova T.A., Zakharov V.A.


We introduce a first-order model of imperative sequential programs and set up formally the unification problem in this model: given a pair of programs $\pi_1$ and $\pi_2$ find a pair of substitutions $(\theta_1,\theta_2)$ such that the instances $\pi_1\theta_1$ and $\pi_2\theta_2$ of these programs are equivalent, i.e. compute the same function. Since functional equivalence of programs is undecidable, we choose its decidable approximation - a strong equivalence, - which is well-known in theory of program schemata. Our main result is a polynomial time unification algorithm for sequential programs w.r.t. strong equivalence of programs.

Text of article


sequential program, logic-and-term equivalence, unification, complexity


Proceedings of the 27-th International Workshop on Unification, June 26, 2013, Eindhoven, EPiC Series, 2013, vol. 123, pp. 36-46.

Research Group

Theoretical Computer Science

All publications during 2013 All publications