状态与效应三角形的配方
摘要：程序语言的语义可以把程序视为状态转换器，或者谓词转换器。最近，作者引入了状态和效果三角形的概念，以范畴论的方式捕捉了这种情况，涉及状态和谓词转换器之间的伴随性。本文利用范畴论中经典的结果之一，即乔恩·贝克的单调性定理的一部分，系统地从伴随构造这样一个状态和效果三角形。该构造的威力通过许多例子来展示，涵盖程序语义中出现的许多单子，包括（概率）幂域。
作者：Bart Jacobs
论文ID：1703.09034
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22