Distributing Retractions, Weak Distributive Laws and Applications to Monads of Hyperspaces, Continuous Valuations and Measures
本文提出分配收缩概念以识别由弱分配律构建的组合单子，证明两者在2-范畴中一一对应，并应用于超空间与连续赋值单子以描述预势单子的代数结构。
2025-11-03 cs.LO math.CT
The costructure-cosemantics adjunction for comodels for computational effects
方程代数理论及其生成的单子可以用来对计算效果进行编码，这是公认的。Power和Shkaravska的一个重要见解是，代数理论T的余模-即，相反类别中的模型Set^op --为评估T编码的计算效果提供了合适的环境。正如Power和Shkaravska已经指出的，取余模型会产生一个从可访问单子到集合上可访问的余单子的函子。在本文中，我们表明，这个函子是一个附加词的一部分-的“结构-共语义附加词”的标题-并进行了彻底的调查，其性质。我们表明，一方面，共语义函子采取它的形象，我们称之为小范畴诱导的前层共单子;另一方面，共结构采取它的形象，在小范畴诱导的前层单子。特别是，一个可访问的单子的共语义comonad将诱导一个明确描述的类别称为其行为类别，编码的静态和动态属性的comodels。类似地，一个可访问的comonad的余结构单子将由编码comonad余代数的静态和动态性质的行为范畴诱导。我们把这些结果联系在一起，表明costructure-cosemantic的附加是幂等的，与不动点的任何一方精确地给出了预层单子和comonads。一路上，我们用计算和数学中的许多例子来说明我们的结果的价值。
2020-11-30 cs.LO math.CT
Monads and Quantitative Equational Theories for Nondeterminism and Probability
概率分布的凸集单子是一个众所周知的工具，用于模拟不确定性和概率计算效果的组合。在这项工作中，我们解除这单子从范畴的集合到范畴的度量空间，通过Hausdorff和Kantorovich度量提升。我们的主要结果是介绍了这解除单子的凸半格的定量方程理论，使用的框架，最近推出的Mardare，Panangelo和Plotkin的定量代数。
2020-05-15 cs.LO
Colimits of Monads
证明了多序集（以及其他类集范畴）上的单子范畴具有余均衡器和强余交。一般图有一个余极限，只要所有涉及的单子保持单态，并有任意大的联合预不动点。相比之下，coequalizers不存在，例如，单子上的（预层）类别的图。对于更一般的范畴，我们推广了文[2]中关于单子上积的结果。我们称一个单子为分离的，如果当限制为单态时，它的单位有一个补。我们证明了每一个具有任意大的联合前缀点的分离单子的集合都有一个余积。并给出了这些余积的具体计算公式。
2014-09-11 cs.LO
Commutative Monads for Probabilistic Programming Languages
在支持概率选择的程序设计语言的语义中，一个长期存在的公开问题是在DCPO范畴上找到概率的交换单子。在本文中，我们提出了三个这样的单子和一个一般的建设，以寻找更多。我们将展示如何使用这些单子提供一个健全的和足够的指称语义的概率定点演算（PFPC）-调用值简单类型的λ演算与混合方差递归类型，长期递归和概率选择。我们还表明，在特殊的情况下，我们认为连续dcpo的，那么所有三个单子符合估值单子的琼斯和我们充分的诱导Eilenberg-Moore类别表明，他们都同构的范畴连续Kegelspitzen的凯梅尔和Plotkin。
2021-01-31 cs.LO cs.PL math.CT
Patterns for computational effects arising from a monad or a comonad
本文提出了基于等式的逻辑证明一阶性质的程序设计语言涉及效果。我们提出了两个对偶推理系统模式，可以实例化与单子或comonads，以用于证明不同的效果的属性。第一种模式提供了可以在单子的Kleisli范畴和相关的comonad的coKleisli范畴中解释的推理规则。第二种模式以双重方式提供了推理规则，这些规则可以在comonad的coKleisli范畴和相关monad的Kleisli范畴中解释。该逻辑结合了一个3层效应系统，用于由纯项和另外两种称为“构造器/观察器”和“修改器”的效应组成的项，以及一个2层系统，用于“最大效应”和“强”方程。每个模式都提供了处理任何monad（分别为comonad）的通用规则，并且可以为每个效果扩展特定的规则。本文提出了两个用例：带有异常的语言（使用标准的一元语义）和带有状态的语言（使用不太标准的共元语义）。最后，我们证明了所得到的状态推理系统是Hilbert-Post完备的。
2013-10-14 cs.LO
On the Behaviour of Coalgebras with Side Effects and Algebras with Effectful Iteration
对于集合上的有限单子$T$和$T$ -代数范畴上的闭函子$F$，我们引入了$F$的ffg-Elgot代数的概念，即允许有限递归方程组的相干解的代数，其效应由单子$T$表示.目的是研究自由ffg-Elgot代数的存在性和构造。为此，我们研究了局部ffg不动点$φF$，即所有具有自由生成载波的$F$ -余代数的上极限，它被证明是初始ffg-Elgot代数。这是我们主要结果的技术基础：ffg-Elgot代数范畴在$T$ -代数范畴上是一元的.
2021-09-09 cs.LO math.CT
Combinatorial structure of type dependency
我们给出了一个帐户的基本组合结构的概念类型依赖。我们这样做是考虑范畴的所有依赖的代数演算，并展示它作为范畴的代数单子上的一个预层范畴。预层范畴的对象编码了一个依赖型组合演算的基本判断，而单子的作用编码了演绎规则;因此，通过给出单子的显式描述，我们得到了类型依赖的组合学的显式说明。我们发现，这种组合是由一种特殊的装饰有序树，熟悉的计算机科学和无辜的游戏语义。此外，我们发现所讨论的单子是一种特别好的单子：它是斯特里特-韦伯意义上的局部右伴随。在未来的工作中，我们将利用这一事实来描述依赖类型理论的神经，并使用二维单子理论的工具来研究依赖类型理论的一致性问题。
2014-02-27 cs.LO math.CT math.LO
A Category-Theoretic Framework for Dependent Effect Systems
Waseda University（早稻田大学）；Boston University（波士顿大学）；National Institute of Informatics（信息学综合研究所）；SOKENDAI（日本综合研究大学院大学）；Tohoku University（东北大学）
本文提出索引分级monad，用于描述依赖效果的类型系统，并展示了其在成本分析、概率界推理等领域的应用。
2026-01-21 cs.LO
The Central Valuations Monad
给出了dcpo与Scott连续函数范畴DCPO上的一个交换赋值单子Z。与[Jia et al.，2021]，我们的新单子Z更大，它包含单位区间[0，1]上沿着下半连续映射的赋值的所有前推像。我们相信，这个新的单子将是有用的，在统计程序设计语言与连续概率选择域理论的指称语义。
2021-11-21 cs.LO math.CT math.GN
Bimonoidal Structure of Probability Monads
我们给出了一个概念性的治疗关节，边缘，并在设置分类概率的独立性的概念。这是通过赋予通常的概率单子（如吉里单子）一个monoidal和opmonoidal结构，相互兼容（即双monoidal结构）。若其基础幺半范畴是Carnival monoidal范畴，则通过交换强度唯一地给出一个双半群结构。然而，如果基础的幺半范畴不是carnival monoidal的，强度不足以保证关节和边缘的所有期望的属性。因此，对于更一般的情况，双单波结构是正确的要求。借助幺半范畴的图演算，我们解释了理论和运算解释。本文基于双单结构给出了随机独立性的定义，它与直觉和文献中的其他方法相一致，适用于Carnival幺半范畴范畴。然后，我们作为一个例子，康托洛维奇单子的范畴内的完全度量空间是一个双单的monad的非carriermonoidal结构。
2020-01-31 cs.LO math.CT math.PR
Natural Transformations as Rewrite Rules and Monad Composition
本文提出用字符串重写方法验证单子复合等范畴论构造，通过重写系统的合流性刻画单子，并给出伴随的重写范畴表征。
2019-01-08 cs.LO
Strongly finitary monads and multi-sorted varieties enriched in cartesian closed concrete categories
本研究将富集范畴中代数簇与强有限单子的对偶等价结果，推广到任意具体笛卡尔闭范畴及多类情形，证明了对应范畴的对偶等价性，并给出了相关实例。
2023-10-06 cs.LO math.CT math.LO
Lifting Coalgebra Modalities and $\mathsf{MELL}$ Model Structure to Eilenberg-Moore Categories
本文在Eilenberg-Moore范畴中为线性逻辑的MELL片段建立模型，通过定义带混合分配律的Hopf单子作为MELL提升单子，证明线性范畴结构可提升至其代数范畴，并利用余代数范畴中的群构造此类单子。
2019-11-06 cs.LO
The quantum instrument monad
University of Innsbruck（因斯布鲁克大学）
提出量子仪器单子 $\mathcal{I}_\mathcal{A}$，作为状态单子的非交换推广，用于建模与量子系统交互的计算效应，并给出集合范畴上的有限版本和可测空间范畴上的测度论版本。
2026-06-29 cs.LO cs.PL math.CT
Logic as a distributive law
我们提出了一种算法，用于从计算演算的正式表示中导出空间行为类型系统。给定2-monad Calc：Catv $\to$ Cat表示范畴上的自由演算并重写，2-monad表示范畴上的自由布尔代数，得到了公式和证明的自由范畴的2-monad Form = BoolAlg + Calc.我们还得到了术语子集的2-monad BoolAlg $\circ$ Calc。公式的解释是自然变换$\interp{-}$：Form $\Rightarrow$ BoolAlg $\circ$ Calc由单子的单位和乘法定义，以及分配律变换$δ$：Calc $\circ$ BoolAlg $\Rightarrow$ BoolAlg $\circ$ Calc。这种解释与柯里-霍华德同构和可实现性都是一致的。我们给出了一个实现的“可能”模态操作符参数化的两个孔长期上下文，并显示，令人惊讶的是，箭头类型的构造函数中的$λ$演算是一个特定的情况。我们还展示了非平凡的公式编码的限制和活性的反射高阶变体的$π$演算的属性。
2016-10-16 cs.LO
Towards Trace Metrics via Functor Lifting
我们研究的可能性，得出度量跟踪语义的一个coalgebraic框架。首先，我们推广了一种技术，系统提升函子从范畴集的集合到范畴PMet的伪度量空间，显示在何种条件下也可以解除自然变换，单子和分配律。通过利用最近的一些工作的抽象决定，这些结果使导迹度量从余代数集。更确切地说，对于集合上的余代数，我们确定它，从而得到单子的Eilenberg-Moore范畴中的余代数。当单子可以提升到PMet时，我们可以为最终的余代数配备行为距离。原余代数的两个状态之间的迹距离是它们在确定余代数中的像之间通过单子单位的距离。我们展示了我们的框架如何适用于不确定自动机和概率自动机。
2015-05-29 cs.LO
Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems
Kleisli范畴中的余代数给出了各种类型的标号变迁系统的迹语义的一般定义。在本文中，我们将这种通用的理论生成概率转换系统，短PTS，任意（可能不可数）的状态空间。在可测空间和可测函数的范畴上，考虑了次概率单子和概率单子（Giry monad）。我们的主要贡献是，存在一个最终的coalgebra在Kleisli类别的这些单子是密切相关的测量理论的扩展定理西格玛有限预措施。事实上，我们得到了一个实用的定义的迹措施的PTS，包括一个众所周知的结果离散概率转移系统的有限和无限的痕迹。最后，我们考虑了两个具有不可数状态空间的系统，并应用我们的理论计算了它们的迹测度。
2013-12-03 cs.LO
Modular specification of monads through higher-order presentations
在二阶方程逻辑的研究中，Fiore和Hur通过生成绑定结构和方程来研究简单类型语言的表示。对于由绑定签名和一组方程组成的每一对，它们关联一个“模型”类别，并且它们给出一个单子性结果，该结果意味着该类别具有一个初始对象，该初始对象是由该对表示的语言。在目前的工作中，我们提出了一个变种，他们的方法，在他们的单子和模块的中心概念的无类型的设置。更确切地说，我们研究，单子集，介绍通过生成（“高阶”）的操作和方程。我们考虑一个概念的2-签名，它允许指定一个单子与一个家庭的绑定操作服从一个家庭的方程，是典型的例子的λ演算的情况下，指定其两个标准的建设（应用和抽象）服从$β$ -和$η$ -等式。因此，这样的2-签名是一对$(Σ,E)$的结合签名$Σ$和用于$Σ$的方程族$E$。这个2-签名的概念已经由Ahrens在稍有不同的上下文中介绍过。我们将每个2-签名$(Σ,E)$与一个“$(Σ,E)$的模型”范畴联系起来;我们说一个2-签名是“有效的”，如果这个范畴有一个初始对象;这个（本质上唯一的）对象下面的单子是“由2-签名指定的单子”。不是每个2-签名是有效的，我们确定了一类2-签名，我们称之为“代数”，是有效的。重要的是，我们的2-签名与它们的模型一起享有“模块性”：当我们将（代数）2-签名粘合在一起时，它们的初始模型也相应地粘合在一起。我们提供了一个计算机形式化我们的主要结果。
2019-03-03 cs.LO math.LO
Monoid Structures on Indexed Containers
本文研究 I-索引容器范畴的张量积幺半群结构，刻画其中幺半群并证明其精确对应 Set^I 上的单子，且用 Cubical Agda 完成形式化。
2025-09-30 cs.LO cs.PL
