Abstract
These mathematical components formalise predicate transformer
semantics for programs, yet currently only for partial correctness and
in the absence of faults. A first part for isotone (or monotone),
Sup-preserving and Inf-preserving transformers follows Back and von
Wright's approach, with additional emphasis on the quantalic
structure of algebras of transformers. The second part develops
Sup-preserving and Inf-preserving predicate transformers from the
powerset monad, via its Kleisli category and Eilenberg-Moore algebras,
with emphasis on adjunctions and dualities, as well as isomorphisms
between relations, state transformers and predicate transformers.
License
Topics
Session Transformer_Semantics
- Isotone_Transformers
- Sup_Inf_Preserving_Transformers
- Powerset_Monad
- Kleisli_Transformers
- Kleisli_Quantaloid
- Kleisli_Quantale