Polynomial time algorithm for checking strong equivalence of program

Abstract

To unify a pair of algebraic expressions t1 and t2 is to find out such a substitution θ that both terms t1θ and t2θ have the same meaning. Unification problem can be extended to computational programs. To unify a pair of programs π1 and π2 is to build two sequences of assignment statements ρ1 : x1 := t1; x2 := t2; … xn := tn and ρ1 : y1 := s1; y2 := s2; … ym := sm, such that both compositions of programs ρ1;π1 and ρ2;π2 are equivalent (i.e. they compute the same function). In this paper we deal with logic-and-term equivalence introduced in 1972 by V. Itkin. This is the most weak decidable equivalence on programs that approximates the functional equivalence. Based on the polynomial-time equivalence checking algorithm for logic-and-term equivalence in the firstorder model of imperative programs we introduce a polynomial-time unification algorithm which computes the most general unifier (ρ1, ρ2) for every pair of sequential imperative (π1, π2) w.r.t. logic-and-term equivalence. After discussing the importance of unification proble for program refactoring and optimization we briefly recall the basic concepts of term substitution theory and theory of program schemata. Then we introduce a formal model of sequential programs we deal with, and finally we present our unification algorithm, prove its correctness and show that its complexity is polynomial on the size of programs to be unified.