An axiomatization of D-scheme strong equivalence

摘要

The class DΩ, Π) of all Dijkstra schemes over (Ω, Π) may be viewed as a Σ-algebra, where the signature Σ is defined as follows: Σ0= {i},where i has constant value I1, Σ1= {Wiπ: π ϵ Π, i = 1 or i = 2}, Σ2= {·} ∪ {Aπ: π ϵ Π}, where I1 is the trivial scheme, W1π and W2π are the while-do operations, Aπ is binary alternation, and · is composition. The strong behavior of a scheme F in D(Ω, Π) is defined to be the (possibly infinite) tree which is the “total unfolding” of F. Two schemes F and G are strongly equivalent if they have the same strong behavior. If D is the Σ-algebra defined above, then strong equivalence is a congruence on D. Denote the resulting quotient by D/∼. The result of this paper is that D/∼ is free in the class of all Σ-algebras which satisfy 1.(i>I1 · x = x · I1 = x,2.(ii)x · (y · z) = (x · y) · z, as well as the following, for each π ϵ Π:3.(iii)Aπ(I1, x · W1π(x)) = W1π(x),4.(iv)Aπ(x · W2π(x), I1) = W2π(x),5.(v)Aπ(x · z, y · z) = Aπ(x, y)· z.`