An Equational Axiomatization of the Algebra of Reducible Flowchart Schemes

The flowchart schemes called “reducible” are of interest because (1) they schematize programs without “go to” statements; (2) for every flowchart scheme there is a reducible one which is step-by-step equivalent to it; (3) they manipulate readily. The reducible flowchart schemes admit both graph-theoretic and algebraic descriptions. A flowchart scheme F with n begins and p exits is reducible iff both (a) for every vertex v there is a begin-path (i.e. a path from a begin vertex) which ends in v (b) for every closed path C there is a vertex vC of C such that every begin path to a vertex of C meets vC. Algebraically: F is reducible iff it can be built up from atomic flowchart schemes (which may be thought of as corresponding to single instructions) and surjective trivial flowchart schemes (which may be thought of as redirecting flow of control) by means of composition (∘), separated pairing (+), and scalar iteration (†). Dropping † yields the accessible, acyclic flowchart schemes. The equational axioms referred to in the title relate ≈-identified (i.e. isomorphism-identified) flowchart schemes by these three operations. The structure freely generated by the set Γ of atomic flowchart schemes is Γ Red, the theory (or multi-sorted algebra) of reducible flowchart schemes. The axioms involving only + and ∘ yield ΓAc, the theory of accessible, acyclic flowchart schemes. Semantical domains which may be used to interpret Γ Red also satisfy these axioms. The set of equational statements true for Γ Red (which are also logical consequences of the axioms) determine a congruence on the algebra of expressions built out of Γ, Sur, +, ∘ and † whose quotient is another description of Γ Red. Thus the expressions built up using these three operations provide an alternative notation for reducible flowchart programs; the purpose of the axioms is to determine when two expressions represent the same schematic program. A similar statement holds for ΓAc.