Healthiness from Duality
Healthiness from Duality
复制标题
来自二元性的健康
DOI：
10.1145/2933575.2935319
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Ichiro Hasuo and Bart Jacobs
中科院分区：
文献类型：
--
作者：
Wataru Hino;Hiroki Kobayashi;Ichiro Hasuo and Bart Jacobs
健康是程序逻辑中一个很老的问题，可以追溯到Dijkstra。它要求对那些谓词转换器进行内在的描述，这些谓词转换器是作为对某类程序的(向后)解释而出现的。对于健康条件，有几个已知的结果：对于确定性的程序，非确定性的，概率的，等等。在我们之前关于所谓的状态-效果三角形的工作的基础上，我们为研究健康条件贡献了一个统一的分类框架。这个框架基于对偶对象诱导的对偶加法和我们的相对Eilenberg-Moore代数的概念。在单子理论、劳维尔理论和丰富的范畴的背景下，后一种概念本身似乎很有趣。
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. This framework is based on a dual adjunction induced by a dualizing object and on our notion of relative Eilenberg-Moore algebra. The latter notion seems interesting in its own right in the context of monads, Lawvere theories and enriched categories.