# Ivannikov Institute for System Programming of the RAS

## Is it possible to unify sequential programs.

#### Authors

Novikova T.A., Zakharov V.A.

#### Abstract

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

#### Keywords

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

#### Edition

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

### Research Group

All publications during 2013 All publications