Two-categories and program structure: data types, refinement calculi, and predicate transformers
David A. Naumann · 1992
The theory of two-categories is used to develop the foundations of programming calculi. Two-categorical tools are used to augment the calculus of predicate transformers with new constructs and to extend algorithmic refinement calculi to data refinement. The presentation is expository and detailed, to help bridge the wide gap between category theory and computing science. The algorithmic refinement calculus of predicate transformers is extended to include constructs for large scale system structure: products and disjoint unions of state spaces along with higher order programs. The preordered category of monotonic predicate transformers is shown to have products, lax exponents, and lax coexponents. Lax coproducts are constructed for disjunctive and for strict finitely conjunctive predicate transformers. A continuous lax coproduct is constructed for boundedly nondeterministic of the order-theoretic structure of classes of predicate transformers satisfying various healthiness conditions. A theory of lax adjunction is used to show uniqueness of lax coproducts and disjunctive lax coexponents, and hence the completeness of their algorithmic refinement laws. (A satisfactory coexponent for conjunctive predicate transformers remains to be found.) The second part of the work investigates conditions under which algorithmic refinement calculi can be extended to data refinement; the criterion for suitability is that their program and proof constructors should preserve simulations. Previous results are extended to preservation of Galois simulations and modifications, and generalized from program constructors to proof constructors and coherence conditions (i.e. two-categories rather than pre-ordered categories). Retract and Galois simulations are preserved by covariant and contravariant two-functors, upward and downward simulations, two-natural transformations, lax junctions and two-junctions, uniform and natural modifications, and dinatural transformations. Modifications between simulations are preserved by the same constructs. As an application, most of the new predicate transformer constructs preserve retract and Galois simulations.