paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Aczel-Mendler Bisimulations in a Regular Category

正则范畴中的 Aczel-Mendler 双模拟
LMCS vol.Volume 21, Issue 32025匹配度 2/10 · 该论文属于范畴论与余代数语义下的双模拟理论研究,虽与形式语义相关,但与用户关注的 PL→AI、AI→PL、浮点程序分析、贝叶斯程序分析及 LLM/Agent 交叉方向几乎没有直接联系。引用 0 inbox
Jeremy Dubut
crossref: 2026-09-10

AI 速览

一句话:将 Aczel-Mendler 双模拟推广到一般正则范畴与 topos,并在不依赖选择公理时证明其对复合封闭及一致性。

Aczel-Mendler 双模拟是系统间计算关系的一种余代数推广,通常假设底范畴满足选择公理以保证双模拟类对复合封闭。本文将该定义适配到一般正则范畴与 topos。作者证明:在无选择公理下双模拟对复合封闭;在更弱条件下与其他余代数表述一致;当范畴满足正则选择公理时与通常定义一致。对于 topos 情形,论证依赖幂对象,并顺带恢复其若干良好性质。最后给出 Stone 空间、名称传递 topos 与环上模等例子。

问题
如何在一般正则范畴和 topos 中定义 Aczel-Mendler 双模拟,并避免通常所需的选择公理,同时保持复合封闭等良好性质?
方法
利用正则范畴与 topos 的范畴结构(尤其是幂对象)重新表述该余代数定义,并与其他 coalgebraic 表述及经典定义进行比较。
评估
通过证明复合封闭性、在不同条件下与已有定义的一致性,并以 Stone 空间、名称传递 topos 和环上模等例子说明该推广的适用性。
原文摘要(Abstract)

Aczel-Mendler bisimulations are a coalgebraic extension of a variety of computational relations between systems. It is usual to assume that the underlying category satisfies some form of the axiom of choice, so that the collection of bisimulations enjoys desirable properties, such as closure under composition. In this paper, we accommodate the definition in general regular categories and toposes. We show that this general definition: 1) is closed under composition without using the axiom of choice, 2) coincides with other types of coalgebraic formulations under milder conditions, 3) coincides with the usual definition when the category satisfies the regular axiom of choice. In particular, the case of toposes heavily relies on power-objects, for which we recover some favourable properties along the way. Finally, we describe several examples in Stone spaces, toposes for name-passing, and modules over a ring.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{abs-2303-04442,
  title = {Aczel-Mendler Bisimulations in a Regular Category},
  author = {Jeremy Dubut},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 3},
  year = {2025},
  doi = {10.46298/lmcs-21(3:23)2025}
}