Axiomatizing schemes and their behaviors (Q1819574)

Flowcharts represent in an abstract way the family of while programs, and flowchart schemes are flowcharts where the individual atomic steps have not been interpreted. It is a classical question to characterize when two flowchart schemes compute the same function under all possible interpretations. This question has been answered: two schemes are equivalent if they produce the same unwinding as infinitary trees. There remains the problem of determining this equivalence in a more down-to- earth way, for example by a characterization using axioms or, more specifically, by an equational theory. The name of C. C. Elgot is connected to the algebraic theory which originates from this problem area. The algebras involved are known by the name Iterative theories. The basic algebraic operations are sequential composition, pairing (or more general tuppling), and iteration. The problem was that these operations were not everywhere defined, and therefore a partial algebra resulted. In the present paper the authors provide an extension of the domain of these operations which turns them into everywhere defined operations. The resulting total algebra is provided with a full and complete equational axiomatization for the required equivalence of program schemes. The paper presumes familiarity with the earlier papers in this area, which it may bring to a temporary conclusion.