分次和加索引单子的2-范畴研究
A 2-Categorical Study of Graded and Indexed Monads
摘要：
在计算效应的研究中，考虑带参数的计算效应的概念是很重要的。例如，当静态估计程序引起的效应范围时，或者研究局部作用域的效应如何从全局作用域的效应中导出时，就需要这样一个概念。扩展了经典的观察，计算效果可以模拟的单子，这些计算效果的参数是由不同的数学结构，包括分级单子和索引单子，这是两个不同的推广普通单子。前者用于研究效果系统的语义，后者用于研究局部状态单子和全局状态单子之间的关系，分别举例说明上述两种情况。然而，尽管它们的重要性，分级和索引单子的数学理论远不如普通单子发达。在这里，我们发展的数学理论的分级和索引单子从2范畴的观点。我们首先介绍了四个2-范畴，并观察到，在其中两个分级单子实际上是单子的2-范畴意义上，类似的索引单子是单子的2-范畴意义上的其他两个。然后，我们明确地构造Eilenberg-摩尔和Kleisli对象的分级单子，和Eilenberg-摩尔对象的索引单子在适当的2-类别中的街的意义。相应的结果分级和索引comonads也如下。我们希望，目前的工作将提供一个理论基础，统一的研究计算效果的参数，或双重（使用comonad变量），计算资源的参数，例如在有界线性逻辑。
英文摘要：
In the study of computational effects, it is important to consider the notion of computational effects with parameters. The need of such a notion arises when, for example, statically estimating the range of effects caused by a program, or studying the ways in which effects with local scopes are derived from effects with only the global scope. Extending the classical observation that computational effects can be modeled by monads, these computational effects with parameters are modeled by various mathematical structures including graded monads and indexed monads, which are two different generalizations of ordinary monads. The former has been employed in the semantics of effect systems, whereas the latter in the study of the relationship between the local state monads and the global state monads, each exemplifying the two situations mentioned above. However, despite their importance, the mathematical theory of graded and indexed monads is far less developed than that of ordinary monads. Here we develop the mathematical theory of graded and indexed monads from a 2-categorical viewpoint. We first introduce four 2-categories and observe that in two of them graded monads are in fact monads in the 2-categorical sense, and similarly indexed monads are monads in the 2-categorical sense in the other two. We then construct explicitly the Eilenberg--Moore and the Kleisli objects of graded monads, and the Eilenberg--Moore objects of indexed monads in the sense of Street in appropriate 2-categories among these four. The corresponding results for graded and indexed comonads also follow. We expect that the current work will provide a theoretical foundation to a unified study of computational effects with parameters, or dually (using the comonad variants), of computational resources with parameters, arising for example in Bounded Linear Logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
