Deciding Equivalence of Functional Schemes for Parallel Programs

摘要

This paper presents two formal systems for proving equivalence of parallel programs. The second system, which is an extension of the first system, is developed on the base of the proof system constructed. A completeness result is obtained for a certain subset of expressions of the second system. In particular, this subset includes all expressions of the first system. The method we use for proving equivalence of parallel programs exhibits a formal resemblance to the method used by SALOMAA for proving equivalence of expressions in the algebra of regular events.