单子与余单子的交互律
计算机科学中的逻辑
2020-01-03 v1 编程语言
范畴论
摘要
我们引入并研究函子-函子与单子-余单子交互律，将其作为描述带效应计算与执行效应之机器行为之间交互的数学对象。单子-余单子交互律是函子-函子交互律的幺半范畴上的幺半对象。我们证明，对于对偶与Sweedler对偶概念的适当推广，与给定函子或余单子交互的最大函子（分别对应）是其对偶，而与给定单子交互的最大余单子是其Sweedler对偶。我们将单子-余单子交互律与有状态运行器相联系。我们证明函子-函子交互律是取Day卷积幺半结构的自函子范畴上的Chu空间。Hasegawa的胶合赋予这些Chu空间所构成的范畴一个幺半结构，其幺半对象即为单子-余单子交互律。
引用
@article{arxiv.1912.13477,
title = {Interaction laws of monads and comonads},
author = {Shin-ya Katsumata and Exequiel Rivas and Tarmo Uustalu},
journal= {arXiv preprint arXiv:1912.13477},
year = {2020}
}