论文标题
用于计算效果的comodels的构造辅助辅助
The costructure-cosemantics adjunction for comodels for computational effects
论文作者
论文摘要
众所周知，方程代数理论及其产生的单元可用于编码计算效应。 An important insight of Power and Shkaravska is that comodels of an algebraic theory T -- i.e., models in the opposite category Set^op -- provide a suitable environment for evaluating the computational effects encoded by T. As already noted by Power and Shkaravska, taking comodels yields a functor from accessible monads to accessible comonads on Set.在本文中，我们表明该函子是标题的“构造 - 化合物相邻”的一部分 - 并对其特性进行了彻底的研究。 我们表明，一方面，Cosemantics Foundator将其形象带到了我们所说的小型类别引起的Presheaf comonads中。另一方面，构造构成了其图像在由小型类别引起的预局部单元中。特别是，可访问的单元的Cosemantics Comonad将由称为其行为类别的明确描述的类别引起，该类别编码comodels的静态和动态属性。同样，可访问的ComoNAD的构造单元将由编码ComoNAD山地的静态和动态特性的行为类别引起。我们通过表明构造 - 化妆品的辅助是基于掌握的，将这些结果绑定在一起，固定点是由Presheaf monads和comonads精确地给出的。在此过程中，我们通过从计算和数学中得出的许多示例来说明结果的价值。
It is well established that equational algebraic theories, and the monads they generate, can be used to encode computational effects. An important insight of Power and Shkaravska is that comodels of an algebraic theory T -- i.e., models in the opposite category Set^op -- provide a suitable environment for evaluating the computational effects encoded by T. As already noted by Power and Shkaravska, taking comodels yields a functor from accessible monads to accessible comonads on Set. In this paper, we show that this functor is part of an adjunction -- the "costructure-cosemantics adjunction" of the title -- and undertake a thorough investigation of its properties. We show that, on the one hand, the cosemantics functor takes its image in what we term the presheaf comonads induced by small categories; and that, on the other, costructure takes its image in the presheaf monads induced by small categories. In particular, the cosemantics comonad of an accessible monad will be induced by an explicitly-described category called its behaviour category that encodes the static and dynamic properties of the comodels. Similarly, the costructure monad of an accessible comonad will be induced by a behaviour category encoding static and dynamic properties of the comonad coalgebras. We tie these results together by showing that the costructure-cosemantics adjunction is idempotent, with fixpoints to either side given precisely by the presheaf monads and comonads. Along the way, we illustrate the value of our results with numerous examples drawn from computation and mathematics.
