The Theory of Traces for Systems with Nondeterminism, Probability, and Termination
本文通过广义幂集构造恢复非确定性与概率系统的迹语义，并与文献中的迹等价性定义进行比较，基于单子与代数理论的相互作用。研究问题为系统迹等价性，核心方法为余代数构造，主要贡献为统一并比较了迹语义。
2022-06-16 cs.LO
Probability and Angelic Nondeterminism with Multiset Semantics
针对幂集与Giry单子间缺乏分配律的问题，提出带天使型非确定性的概率克林代数及自动机类，用多重集分布实现语义，得出克林定理、余代数理论等关键结果，解决理论障碍。
2025-04-17 cs.FL cs.LO cs.PL
Sum and Tensor of Quantitative Effects
本研究受代数计算效应组合工作启发，构建定量代数效应的和与张量组合理论，证明其对应单子的范畴和与张量，提出定量效应转换器，并首次为多种共代数结构给出定量代数公理化。
2024-10-28 cs.LO
Exploring the Boundaries of Monad Tensorability on Set
我们研究了单子上的组合操作，相当于大方程理论。具体来说，我们讨论张量的存在，这是理论的组合，施加相互交换的操作从组件的理论。因此，他们扩展了两个理论的总和，这只是他们无限制的组合。理论的张量出现在几个上下文中;特别是在程序设计语言的语义中，全局状态的单子Transformer由张量给出。我们提出了两个主要结果：我们通过提出两个反例，其中一个涉及有限幂集（即连接半格理论），证明了两个单子的张量一般不需要存在;这解决了一个长期存在的开放问题，并与最近的结果形成对比，这些结果排除了以前预期的反例。另一方面，我们表明，张量有界幂集单子确实存在从可数幂集向上。
2013-09-17 cs.LO
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
Universal Quantitative Algebra for Fuzzy Relations and Generalised Metric Spaces
本文推广 Mardare 等人的定量代数理论，使载体可为模糊关系或广义度量空间且运算无需非扩张，并给出完备证明系统、自由代数存在性、伴随严格单子性及 monad 的定量等式表示。
2024-12-02 cs.LO
Scoped Effects as Parameterized Algebraic Theories
本文将 scoped effects 翻译为 parameterized algebraic theories 的变体，为其等式推理和 monad 刻画提供新框架，并通过多个已知模型验证该方法。
2024-05-20 cs.LO cs.PL math.CT
Probability monads with submonads of deterministic states - Extended version
概率论可以作为一个交换单子所体现的计算效果进行综合研究。在最近提出的马尔可夫范畴，一个工作与Kleisli范畴的抽象，然后定义确定性态射方程的复制和丢弃。由此产生的“纯粹的”和“确定性的”之间的差异，使我们调查的“清醒”的对象的概率单子，这两个概念相吻合。我们提出自然条件的概率单子，使我们能够确定清醒的对象，并定义一个幂等清醒函子。我们的框架适用于许多感兴趣的例子，包括可测空间上的吉里单子，并允许我们锐化以前给出的版本的德菲内蒂定理的马尔可夫类别。这是2022年计算机科学（LICS）会议接受的论文的扩展版本。在本文件中，我们包括更多的数学细节，包括所有的证明，在出版的版本中给出的陈述和结构。
2022-04-14 cs.LO math.CT math.PR
Presenting with Quantitative Inequational Theories
它引起了我和（S.，Rozowski，Silva，Rot，2022），许多过程演算可以通过代数表示它们指定的转移系统的分支结构来获得。例如，标记的变迁系统分支成变迁集，由变迁生成的自由半格中的项。在集范畴中解释方程理论有着不希望的局限性，我们希望有更多的例子来说明其他范畴中的表述。在这篇简短的文章中，我将讨论偏序集和单调映射范畴中的单子表示。我专注于定量单子，即自由模有序半环，并给出其中之一的充分条件，以解除单子的集范畴。我还描述了有序半环，这对指定无保护递归调用很有用。例子包括有序概率论和有序半格。
2022-10-21 cs.LO math.LO
Breaking a monad-comonad symmetry between computational effects
计算效应通常可以在单子的Kleisli范畴或共单子的coKleisli范畴中解释。monads和comonads之间的二元性一般对应于构造和观察之间的对称性，例如在提出异常和查找状态之间。由于附加的性质，我们可以更进一步：monad的coKleisli-on-Kleisli范畴提供了关于给定构造的一种观察，而comonad的Kleisli-on-coKleisli范畴对偶地提供了关于给定观察的一种构造。在前面的示例中，这会导致捕获异常并更新状态。然而，计算效应的解释通常是基于一个不是自对偶的范畴，如集合范畴。这导致了单子-共单子二元性的打破。例如，在分配范畴中，状态效应比例外效应具有更好的性质。这句话为处理异常的常用机制提供了一个新的观点。本文的目的是建立一个等式的异常处理语义的基础上coKleisli-on-Kleisli类别的单子异常。我们专注于n元函数和条件。我们提出了一个程序员的语言异常，我们证明，它具有所需的行为，n元函数和条件。
2014-02-05 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
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
Free algebras of topologically enriched multi-sorted equational theories
本文将多类等式理论推广到在 Set 上拓扑的对称幺半范畴 V 中强化的情形，证明自由 T-代数可由底层经典理论的自由代数提升得到，并给出显式归纳描述。
2023-08-18 cs.LO math.CT math.GN
Enriched algebraic theories and monads for a system of arities
在最少的假设条件下，我们一般地发展了关于特定的群系统$j:\mathcal{J} \hookrightarrow \mathcal{V}$的对称么半群闭范畴$\mathcal{V}$中泛代数的基本理论。Lawvere的代数理论的概念推广到这一背景，导致了单排序$\mathcal{V}$ -丰富的$\mathcal{J}$ -余张量理论，或简称$\mathcal{J}$ -理论。对于$\mathcal{V}$和$\mathcal{J}$的适当选择，这样的$\mathcal{J}$ -理论包括Borceux和Day的丰富的代数理论，Power的丰富的Lawvere理论，Linton 1965年工作的方程理论，以及Dubuc的$\mathcal{V}$ -理论，它们通过取$\mathcal{J} = \mathcal{V}$恢复，并且对应于$\mathcal{V}$上的任意$\mathcal{V}$ -单子。我们确定了一个适度的条件$j$，需要的$\mathcal{V}$范畴的$\mathcal{T}$ -代数存在，是一元以上的$\mathcal{V}$的每一个$\mathcal{J}$ -理论$\mathcal{T}$，即使当$\mathcal{T}$是不小的，$\mathcal{V}$是既不完整，也不是上完全的。我们证明了$j$满足这个条件的充要条件是$j$将$\mathcal{V}…
2016-04-26 cs.LO math.CT math.LO
Persistent Magnitude Homology for Quantitative Equational Theories
Friedrich-Alexander Universität Erlangen-Nürnberg（弗里德里希-亚历山大大学埃尔兰根-纽伦堡分校）
该研究证明大小同调是长度滤过的相伴分次，将其应用于定量等式理论并给出条形稳定性估计与公理强度衡量方法，计算了四个不同度的示例。
2026-09-17 cs.CG cs.LG cs.LO
Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
本文研究图上概率编程语言的语义模型，建立其与图子的联系，证明良态等式理论与图子一一对应，并通过Markov范畴、测度论概率和名义集合三种构造证明所有图子均源于等式理论，从而构建了图概率编程新模型。
2023-12-28 cs.LO cs.PL math.PR
