计算效应 comodel 的 costructure-cosemantics 伴随

众所周知,等式代数理论及其生成的单子可用于编码计算效应。Power 与 Shkaravska 的一个重要洞见是,代数理论 T 的 comodel——即在相反范畴 Set^op 中的模型——为求值由 T 编码的计算效应提供了合适环境。正如 Power 与 Shkaravska 已指出的,取 comodel 得到一个从 Set 上可访问单子到可访问余单子的函子。在本文中,我们证明该函子是某个伴随的一部分——即标题中的“costructure-cosemantics 伴随”——并彻底研究其性质。我们证明,一方面,cosemantics 函子将其像落在我们称之为由小范畴诱导的余单子之中;另一方面,costructure 将其像落在由小范畴诱导的单子之中。特别地,可访问单子的 cosemantics 余单子将由显式描述的行为范畴诱导,该范畴编码了 comodel 的静态与动态性质。类似地,可访问余单子的 costructure 单子将由编码余单子余代数静态与动态性质的行为范畴诱导。我们通过证明 costructure-cosemantics 伴随是幂等的,且两侧的不动点恰为由预层单子与余单子给出,将这些结果联系在一起。在此过程中,我们用来自计算与数学的众多例子说明了我们结果的价值。