Two-sided unification is NP-complete.

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.

Full text of the paper in pdf

Keywords

program, strong equivalence, substitution, complexity, tiling problem, NP-completeness.

Edition

Proceedings of the 28th International Workshop on Unification (UNIF-2014), RISC-Linz Report Series, 2014, JKU Linz, Vienna, Austria, vol. 6, p. 55-61.

Research Group

Theoretical Computer Science

All publications during 2014

All publications