# Healthiness from Duality

arXiv: https://arxiv.org/abs/1605.00381 · HTML: https://mlsanity.com/paper/1605.00381/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 May 2016.

## Built on by (most cited first, 1 of 1)

- [Weighted Programming](https://mlsanity.com/paper/2202.07577/) (2022)

## Abstract (arXiv)

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.