Abstract
Assertional categories provide a general algebraic framework for the denotation of programs. While the axioms deal exclusively with the abstract structure of coproducts, it is possible to express Boolean structure, loop-free constructs and predicate transformers and to deduce basic properties associated with propositional dynamic logic. At the foundational level, new "quarks" to build the atomic constructions of programs are espoused, leading to a new categorical duality principle for predicate transformers (based on a semilattice completion by ideals) and to the "grand unification principle" that "composition determines semantics". The first-order theory of assertional categories is more general than dynamic logic in that nondeterminism may include repetition count, that is, f + f need not be f. On the other hand, an adaptation of a theorem of Kozen shows that, at least for iteration-free sentences about predicate transformers, semantics is standard. Several algebraic characterizations of Dijkstra's definition of determinism are offered and one leads to a technique to reduce loop-free expressions to guarded commands. Axioms for iteration include a "uniformity principle" that "related programs have related iterates" and the Segerburg induction axiom follows.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. A. Arbib and E. G. Manes, Functorial iteration, Notices Amer. Math. Soc. 25, 1978, A-381.
M. A. Arbib and E. G. Manes, Partially-additive categories and the semantics of flow diagrams, J. Algebra 62, 1980, 203–227.
M. A. Arbib and E. G. Manes, The pattern-of-calls expansion is the canonical fix-point for recursive definitions, J. Assoc. Comput. Mach. 29, 1982, 557–602.
J. Backus, Can programming be liberated from the von Neumann Style? A functional style and its algebra of programs, Commun. Assoc. Comput. Mach. 21, 1978, 613–641.
J. Backus, The algebra of functional programs: function level reasoning, linear equations and extended definitions, in J. Diaz and T. Ramos (eds.), Formalization of programming concepts, Lecture Notes in Computer Science 107, Springer-Verlag, 1981, 1–43.
S. L. Bloom, C. C. Elgot and J. B. Wright, Solutions of the iteration equation and extensions of the scalar iteration operation, SIAM J. Comput. 9, 1980, 25–45.
S. L. Bloom, C. C. Elgot and J. B. Wright, Vector iteration in pointed iterative theories, SIAM J. Comput. 9, 1980a, 525–540.
S. L. Bloom and Z. Esik, Axiomatizing schemes and their behaviors, J. Comput. Sys. Sci. 31, 1985, 375–393.
J. H. Conway, Regular Algebra and Finite Machines, Chapman and Hall, London, 1971.
E. W. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976.
S. Eilenberg, Automata, Languages, and Machines, Vol. A, Academic Press, 1974.
S. Eilenberg and S. Mac Lane, General theory of natural equivalences, Trans. Amer. Math. Soc. 58, 1945, 231–294.
C. C. Elgot, Monadic computation and iterative algebraic theories, in H. E. Rose and J. C. Shepherdson (eds.), Proc. Logic Colloq. '73, North-Holland, 1975, 175–230.
C. C. Elgot and J. C. Shepherdson, An equational axiomatization of reducible flowchart schemes, IBM Research Report RC-8221, April 1980; in S. L. Bloom (ed.), Calvin C. Elgot, Selected Papers, Springer-Verlag, 1982, 361–409.
C. J. Everett and S. Ulam, Projective algebra I, Amer. J. Math. 68, 1946, 77–88.
M. J. Fischer and R. E. Ladner, Propositional dynamic logic of regular programs, J. Comput. Sys. Sci. 18, 1979, 194–211.
P. Freyd, Abelian Categories, Harper and Row, 1964.
D. Harel, First-order Dynamic Logic, Lecture Notes in Computer Science 68, Springer-Verlag, 1979.
C. A. R. Hoare, An axiomatic basis for computer programming, Comm. Assoc. Comput. Mach. 12, 1969, 576–580, 583.
B. Jonsson and A. Tarski, Representation problems for relation algebras, abstract 89t, Bull. Amer. Math. Soc. 54, 1948, 80.
D. Kozen, A representation theorem for models of *-free PDL, in J. W. de Bakker and J. Van Leeuwen (eds.), Automata, Languages and Programming, ICALP '80, Lecture Notes in Computer Science 85, Springer-Verlag, 1980, 351–362.
D. Kozen, On induction vs. *-continuity, in E. Engeler (ed.), Logics of Programs, Lecture Notes in Computer Science 131, 1981, 167–176.
F. W. Lawvere, Functorial semantics of algebraic theories, Ph.D. Dissertation, Columbia University, 1963.
R. C. Lyndon, The representation of relation algebras, Ann. Math. 51, 1950, 707–729.
E. G. Manes, Additive domains, in A. Melton (ed.), Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science 239, Springer-Verlag, 1985, 184–195.
E. G. Manes, Guard modules, Algebra Universalis 21, 1985a, 103–110.
E. G. Manes, A transformational characterization of if-then-else, to appear.
E. G. Manes and M. A. Arbib, Algebraic Approaches to Program Semantics, Springer-Verlag, 1986.
E. G. Manes and D. B. Benson, The inverse semigroup of a sum-ordered semiring, Semigroup Forum 31, 1985, 129–152.
J. C. C. McKinsey, Postulates for the calculus of binary relations, J. Symbolic Logic 5, 1940, 85–97.
R. Milne and C. Strachey, A Theory of Programming Language Semantics, Parts a and b, Chapman and Hall, London, 1976.
B. Mitchell, Theory of Categories, Academic Press, 1965.
E. Nelson, Iterative algebras, Theoret. Comp. Sci. 25, 1983, 67–94.
R. Parikh, Propositional dynamic logics of programs: a survey, in E. Engeler (ed.), Logic of Programs, Lecture Notes in Computer Science 125, 1981, 102–144.
V. R. Pratt, Models of program logics, Proc. 20th IEEE Symp. Found. Comp. Sci., IEEE 79CH1471-2C, 1979, 115–122.
V. R. Pratt, Dynamic algebras and the nature of induction, Proc. 12th ACM Symposium on Theory of Computing, May 1980, 22–28.
J. Reiterman and V. Trnková, Dynamic algebras which are not Kripke structures, Proc. 9th Symposium on Mathematical Foundations of Computer Science, Aug. 1980, 528–538.
K. Segerburg, A completeness theorem in the modal logic of programs, Notices Amer. Math. Soc. 24, 1977, A-522.
M. E. Steenstrup, Sum-ordered partial semirings, Ph.D. Dissertation, University of Massachusetts at Amherst, 1985.
M. H. Stone, The theory of representations for Boolean algebras, Trans. Amer. Math. Soc. 40, 1936, 37–111.
J. E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, M. I. T. Press, 1977.
N. V. Subrahmanyam, Boolean vector spaces I, Math. Zeit. 83, 1964, 422–433.
N. V. Subrahmanyam, Boolean vector spaces II, Math. Zeit. 87, 1965, 401–419.
N. V. Subrahmanyam, Boolean vector spaces, III, Math. Zeit. 100, 1967, 295–313.
A. Tarski, On the calculus of relations, J. Symbolic Logic 6, 1941, 73–89.
J. Tiuryn, Unique fixed points vs. least fixed points, Theoret. Comput. Sci. 13, 1981, 229–254.
E. G. Wagner, S. L. Bloom and J. W. Thatcher, Why algebraic theories?, in M. Nivat and J. C. Reynolds (eds.), Algebraic Methods in Semantics, Cambridge Univ. Press, 1985, 607–634.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manes, E. (1988). Assertional categories. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Language Semantics. MFPS 1987. Lecture Notes in Computer Science, vol 298. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19020-1_5
Download citation
DOI: https://doi.org/10.1007/3-540-19020-1_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19020-2
Online ISBN: 978-3-540-38920-0
eBook Packages: Springer Book Archive