Algorithm for Verifying the Equivalence of Linear Unary Recursive Programs on Ordered Semigroup Scales

摘要

A new method for solving the problem of equivalence of linear unary recursive programs is proposed. The main idea behind this method is to reduce the equivalence problem to known problems on graphs and to problems in group theory. A class of program semantics is singled out for which the problem of the equivalence of the programs in question is solvable in polynomial time by the proposed method.