Healthiness from Duality

TL;DR

This paper develops a unified categorical framework to characterize healthiness conditions in program logics, extending classical results to a broader, more abstract setting using duality and algebraic structures.

Contribution

It introduces a novel categorical approach based on dual adjunctions and Eilenberg-Moore algebras to analyze healthiness conditions across various program types.

Findings

Unified framework for healthiness conditions

Application of duality via dualizing objects

Role of relative Eilenberg-Moore algebras in program semantics

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.