A Recipe for State-and-Effect Triangles

Abstract

In the semantics of programming languages one can view programs as state transformers, or as predicate transformers. Recently the author has introduced state-and-effect triangles which capture this situation categorically, involving an adjunction between state- and predicate-transformers. The current paper exploits a classical result in category theory, part of Jon Beck's monadicity theorem, to systematically construct such a state-and-effect triangle from an adjunction. The power of this construction is illustrated in many examples, covering many monads occurring in program semantics, including (probabilistic) power domains.

References in corpus (3)

• A Recipe for State-and-Effect Triangles
• Probabilistic Monads, Domains and Classical Information
• On the equivalence of state transformer semantics and predicate transformer semantics

Cited by in corpus (6)

• A Recipe for State-and-Effect Triangles
• The Category of Von Neumann Algebras
• Dagger and Dilation in the Category of Von Neumann algebras
• Distances between States and between Predicates
• Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL
• Effectuses in Categorical Quantum Foundations