Healthiness from Duality
Abstract
Healthiness is a good old question in program logics that dates back to Dijkstra. It asks for an intrinsic characterization of those predicate transformers which arise as the (backward) interpretation of a certain class of programs. There are several results known for healthiness conditions: for deterministic programs, nondeterministic ones, probabilistic ones, etc. Building upon our previous works on so-called state-and-effect triangles, we contribute a unified categorical framework for investigating healthiness conditions. We find the framework to be centered around a dual adjunction induced by a dualizing object, together with our notion of relative Eilenberg-Moore algebra playing fundamental roles too. The latter notion seems interesting in its own right in the context of monads, Lawvere theories and enriched categories.
Cite
@article{arxiv.1605.00381,
title = {Healthiness from Duality},
author = {Wataru Hino and Hiroki Kobayashi and Ichiro Hasuo and Bart Jacobs},
journal= {arXiv preprint arXiv:1605.00381},
year = {2016}
}
Comments
13 pages, Extended version with appendices of a paper accepted to LICS 2016