Weak equivalence in a class of structured program schemes (Q797988)

Given predicates \(P_ i\) and biscalar \(F_ i\), \(l\leq i\leq n\), the operation \(\Omega_ n(P_ 1,F_ 1,...,P_ n,F_ n)\) yields a scheme. For any positive integer \(n,BJ_ n\) 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 \(\Omega_ i\), 1\(\leq i\leq n\). \(BJ_ 1\) 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 \(BJ_ n\) schemes are presented. It follows from the proof of the completeness of these axioms that there is a unique minimal strongly free \(BJ_ n\) scheme weakly equivalent to a given strongly free \(BJ_ n\) 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 \(F_ M\) weakly equivalent to F in time proportional to the square of the number of nonexit vertices of F.