This paper deals with equivalence checking problem for a class of recursive programs. These programs is an abstract model of computation used for the analysis of functional programs. A recursive program is defined as a set of functional equations. The left-hand side of every equation is a functional variable (a function specified by the program), and the right-hand side of an equation is a term which includes functional variables and constants (basic functions). A recursive program is called monadic if all functions occurred in it are unary, and it is called linear if every right-hand side term in the program includes one functional variable at most. The semantics of recursive programs under consideration is defined by means of interpretation (models) of Propositional Dynamic Logic (PDL). In fact, the semantics of basic functions is specified by PDL frames. A frame is called balanced if for every pair of basic terms these terms yield different results only if they have different length. The paper presents a novel uniform technique for reducing equivalence checking problem for linear monadic recursive programs on balanced frames to the well known word problem in semigroups. Using this technique we show that equivalence checking problem for recursive programs with commutative basic functions is decidable in polynomial time.

recursive program, semantics, Propositional Dynamic Logic, equivalence checking problem, semigroup, decision procedure, polynomial time

Mathematical problems and theory of numerical methods