Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
433749 | Theoretical Computer Science | 2015 | 28 Pages |
Abstract
We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs' recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: (1) different notions of modality (such as “may” vs. “must”) are captured by Eilenberg–Moore algebras; (2) nested alternating branching—like in games and in probabilistic systems with nondeterministic environments—is modularly modeled by a monad on the Eilenberg–Moore category of another.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Ichiro Hasuo,