Weak equivalence in a class of structured program schemes

摘要

Given predicates Pi and biscalar schemes Fi, 1 ⩽ i ⩽ n, the operation Ωn(P1, F1,…,Pn, Fn) yields a scheme For any positive integer n, BJn is defined to be the least class of schemes containing the trivial scheme and the atomic schemes closed under composition, binary alternation, and the operations Ωi,1 ⩽ i ⩽ n. BJ1 is the well-known class of D-schemes. Two program schemes are weakly equivalent if they compute the same partial function in every interpretation: equational axioms for the weak equivalence of strongly free BJn schemes are presented. It follows from the proof of the completeness of these axioms that there is a unique minimal strongly free BJn scheme weakly equivalent to a given strongly free BJn scheme. This result is used to design an algorithm which optimizes strongly free D-schemes: given a strongly free D-scheme F, it is possible to construct the unique minimal strongly free D-scheme FM weakly equivalent to F in time proportional to the square of the number of nonexit vertices of F.