On an equivalence checking technique for algebraic models of programs
Римма Ивановна Подловченко · Programming and Computer Software · 2011
In the paper, the equivalence checking problem for program schemas in balanced semigroup models of programs is studied. A method for constructing algorithms to resolve this problem is proposed in the case where a semigroup model of programs possesses the left cancellation property h 1 h 2 = h 1 h 3 ⟹ h 2 = h 3. The equivalence checking problem is shown to be decidable in time that polynomially depends on size of the schema being checked if the balanced semigroup model of programs possesses additionally the right cancellation property h 2 h 1 = h 3 h 1 ⟹ h 2 = h 3.