研究：Profunctor 双范畴、富范畴重写、双范畴余极限

相关研究：Profunctor 双范畴、富范畴重写、双范畴余极限

“Double categories of profunctors” 相关研究综述

本文聚焦于 Yuto Kawase 于 2025 年发表的论文《Double categories of profunctors》，以及围绕该论文所涉及的三个主要研究方向：（1）profunctor 双范畴结构的理论发展，（2）范畴富结构（enrichment）与重写系统的结合，以及（3）双范畴 余极限（double-categorical colimit）的概念及其具体应用。

Profunctor 双范畴的理论发展

基础概念与历史背景： “profunctor”（又称 distributor）广义上是范畴之间的一种关联，是 functor 的推广。早在 20 世纪 80 年代，Wood 等人就指出：固定基底（如集合，或更一般的某种“富结构”）上所有范畴、函子与 profunctor 可以自然地组织成一种 拟箭装备（proarrow equipment），这实际上就是一种特殊的双范畴结构epe.bac-lac.gc.ca。后来，Shulman（2008）将这种结构形式化地刻画为“框架双范畴”（framed bicategory），奠定了 双范畴 理论在形式范畴论中的基础。

虚拟双范畴与严格刻画： Kawase 的论文将目光投向虚拟双范畴 (virtual double category) 的视角，对象是富范畴 (enriched category)、1-态射是函子（作为“垂直”箭头）以及 profunctor（作为“水平”箭头），2-态射为相应的自然变换或方块态射。论文的主要成果是引入双范畴意义下的余极限概念，并以此严格表征了上述由富范畴、函子和 profunctor 组成的虚拟双范畴arxiv.org。这种表征在 等价 意义下是严格的：虚拟双范畴之间保持等价，而在对象层面上富范畴则保持同构arxiv.org。值得注意的是，作者并未将富结构简化或去除，而是以富范畴作为基本语言，在一个称为“增广的虚拟双范畴”（augmented VDC）的框架中进行组合和粘合。这种方法确保了拼贴图（pasting diagram）的直观表达，并使富结构在双范畴中原生地得到支持arxiv.org。

近期拓展与相关工作： Profunctor 双范畴结构近年来持续得到发展与推广。例如，Schultz (2015) 提出了正则和完全（regular & exact）的（虚拟）双范畴的定义，证明了这些定义下的一系列基本性质，平行了经典范畴论中正则范畴/完全范畴的许多结果arxiv.org。Lambert (2021) 和 Hoshino & Nasu (2025) 则关注 关系 与 Span 这类特殊 profunctor 的双范畴结构。其中，Hoshino 和 Nasu 将 关系的双范畴 推广到带有稳定正交分解系统的情形，提出了相对关系双范畴的概念arxiv.org。他们通过两种方法刻画了此类双范畴：其一基于一般化的理解方案（comprehension scheme），其二完全在双范畴内部定义一类特殊的垂直态射arxiv.org。这一框架统一了以往对 Span 和关系双范畴的各种刻画，并将它们与不同类型的分解系统相对应arxiv.org。总体来看，过去二十年中关于 profunctor 双范畴的研究逐步形成了完善的理论体系，从一般装备理论（equipments）到增强的虚拟双范畴，再到对特定结构（如关系、Span）的分类刻画，每一步都在丰富双范畴理论的内涵。

富范畴理论与重写系统的结合

重写系统的范畴语义： 重写系统（如项重写、图重写）传统上通过推导规则的应用顺序来描述计算过程。范畴论提供了一种高层次的语义视角：例如，José Meseguer 提出的重写逻辑可以被看作是由给定理论 $T$ 所生成的自由幺半群 2-范畴（monoidal 2-category）link.springer.com。换言之，一个重写理论的推导过程可对应于一个 2-范畴中的2-态射序列。而更进一步的Tile 模型（Montanari 和 Gadducci 等人在 90 年代提出的 拼贴逻辑）扩展了重写逻辑，通过在推导过程中显式考虑副作用和同步，采用了双范畴作为语义基础link.springer.com。正如 Meseguer 和 Montanari 比较两种逻辑时指出的：对于同一个理论 $T$，重写逻辑语义可视为 $T$ 所生成的自由幺半群 *2-*范畴，而 tile 逻辑语义则是 $T$ 所生成的自由幺半群 双范畴link.springer.com。这意味着在 tile 逻辑中，每一步重写（包括上下文和交互）都对应双范畴中的一个方块2-态射；重写策略因此可以作为双范畴中的“水平”合成来表现，而无需借助外部的控制结构。

富结构在重写中的运用： 将范畴富结构引入重写系统，可以更精细地刻画重写的限制和策略控制。例如，2-范畴本身可看做是富于 $\mathbf{Cat}$（小范畴范畴）上的范畴，因此 2-范畴 = Cat-富范畴。这一观察启发了对Sesqui-范畴（欠互换律的“1.5-范畴”）以及其他富范畴的利用，以建模复杂的重写语义independent.academia.edu。实际上，早期研究者已指出：许多重写结构可以视作在某种单对象（或更高维）范畴上富化的结果，例如带有约束或上下文的重写可对应于在偏序或其它单纲范畴上富化的范畴模型independent.academia.edu。特别地，条件重写逻辑、策略组合等可以用 富范畴 或 伪范畴 来刻画，使得规则的应用策略成为范畴结构中的一等公民，而不再是额外指定的控制流程。这与 Kawase 提出的观点不谋而合：在他的双范畴框架下，重写策略能够作为双向箭头（方块态射/2-态射）自然出现，组合策略本身就是范畴论意义下的态射。这一思路潜力巨大，意味着我们可以运用范畸论工具，直接在 DSL（领域专用语言）的语义层面对重写规则的组合、执行调度以及控制逻辑进行操作和分析。

相关实例与进展：Tile logic 是富结构结合重写的经典示例：它通过对称单模双范畴来建模并发系统中的规则拼接，为组合式语义提供了模块化逻辑框架link.springer.com。近年来，这一思想延伸到各种开放系统和并发模型中。比如 开放 Petri 网、开放电路 等系统可以建模为 结构化余 span 的双范畴，其中水平1-态射表示系统片段的开放组合，2-态射表示这些组合之间的变换或等价。Courser (2020) 的研究展示了如何利用结构化 cospan 建立对开放系统的双范畴语义：在满足一定条件（如基础范畴存在有限余极限且函子 $L: \mathsf{A}\to\mathsf{X}$ 左伴随）的情况下，我们可构造一个对称单模双范畴，其对象是系统接口，水平态射是结构化 cospan 所表示的开放系统，而且可以定义 2-态射表示系统之间的等价或变换arxiv.org。这种双范畴语义已经成功应用于开放的电路、Markov 过程和 Petri 网等领域，体现出范畴论在描述并发和重写计算方面的强大能力arxiv.org。总的来说，将富范畴与重写系统相结合，使我们能够以代数方式刻画重写规则的执行及其调度策略，从而为编译器优化、模型检验等提供坚实的数学语义基础。

双范畴余极限的概念与应用

定义与背景：双范畴余极限（double-categorical colimit）指的是在双范畴内部定义的“泛胚”结构，类似于 2-范畴或 1-范畴中的余极限，但需同时考虑水平态射和垂直态射的复合关系。Kawase (2025) 正是通过引入这一新概念，严格刻画了富范畴/函子/profunctor 组成的虚拟双范畴arxiv.org。在他的框架中，一个双范畴余极限可以视为某种方形拼接的泛性质：满足一定条件的2-格图表（diagram）在双范畴中存在“最优”粘合，从而泛映射出其它一切此类粘合。引入双范畴余极限的好处在于，我们可以在双范畴层次讨论完备性、余完备性等概念，并将经典范畴论中的构造提升到更高维的情景中。

应用1：Profunctor Collage（拼贴）的胶合：Collage（拼贴范畴）是双范畴余极限的一个典型实例。给定一个范畴 $\mathcal{C}$ 和 $\mathcal{D}$ 之间的 profunctor $M:\mathcal{C}\nrightarrow\mathcal{D}$，其 collage 可以理解为将 $\mathcal{C}$ 和 $\mathcal{D}$ “胶合”在一起所得的范畴，其中新增的态射正是来自 $M$ 的元素。这种拼贴构造在双范畴 $\mathbf{Prof}$（对象是范畴，水平1-态射是 profunctor）中体现为一个双范畴余极限：collage 满足对应的泛性质，使得任何将 $M$ 映射为双范畴方块的拼合，都要经由这个 collage 唯一地分解arxiv.org。“范畴-函子-profunctor”装备 $\mathbf{Prof}$ 中确实存在这样的正常拼贴 (normal collage) 且满足泛性质arxiv.org。这一构造在数据库等领域有直接应用：例如，Schultz 等人将数据库模式之间的态射看作 profunctor，并利用 collage 来将不同模式整合成统一视图arxiv.org。在他们对代数数据库的模型中，每个 profunctor（模式与代数理论之间的关系）都有一个 collage，其存在性等价于装备满足一定的完备性条件arxiv.orgarxiv.org。可见，collage 作为双范畴余极限为跨范畴的信息整合与迁移提供了范畴论工具arxiv.org。

应用2：形式范畴论中的 Kan 扩张与极限： 在增广虚拟双范畴框架下，许多经典的形式范畴论构造（如 Kan 扩张、伴随等）都可以通过双范畴中的（余）极限来刻画。例如，Koudenburg (2024) 在增广 VDC 中发展形式范畴论时，就利用了双范畴的完备/余完备结构来定义 Kan 扩张、Yoneda 镶嵌等概念，使其不依赖于传统的单一基底范畴researchgate.net。双范畴余极限在此扮演关键角色：它允许我们同时考虑横向（如 profunctor 组合）和纵向（如函子复合）的限制条件，定义出 2-维泛性质 的扩张与延拓。这不仅推广了 2-范畴中的相应概念，也为某些高级构造（例如相对 Monad 的 Nerve 定理等）提供了统一视角arxiv.org。值得一提的是，双范畴余极限的思想也和理解结构（comprehension）密切相关。Hoshino & Nasu (2025) 在刻画关系双范畴时，就采用了一种广义的理解结构，其本质可看作在双范畴中某类特殊余极限的存在性条件arxiv.org。总而言之，在高阶范畴理论内部，引入双范畴（余）极限极大地丰富了我们可讨论的范畴性质，使许多原本需要在 2-范畴或双范畴外讨论的问题能够在内部自然解决。

应用3：重写和开放系统的组合： 双范畴余极限在计算系统的语义组合方面也有直接用途。例如，在双推出现图重写（DPO graph rewriting）中，一个重写步骤对应于两个 pushout 的组合，而 pushout 正是范畴中的一种余极限。在双范畴视角下，我们可以将 DPO 重写形式化为 Span 双范畴中的一个水平拼接：左图 $L\leftarrow K \rightarrow G$ 和右图 $R\leftarrow K \rightarrow G$ 的 span 通过一个水平余推（horizontal colimit）合成为 $G$ 重写到 $H$ 的 2-态射方块。这种表示揭示了重写步骤的泛性质：$H$ 是使得方块满足特定通 UNIVERSAL 性质的“最优”粘合图。类似地，在结构化 cospan 构造的开放系统语义中，每一次将开放系统并联（合并接口）都需要在基础范畴中形成 pushout。这要求基础范畴具有相应的余极限，从而保证双范畴中的水平合成存在arxiv.org。Baez 和 Courser 等人的工作表明，当基础范畴满足有限余极限存在且 $L$ 有左伴随时，我们不仅能构造结构化 cospan 的范畴，而且能得到富含余极限的双范畴结构，使任意两个开放系统的拼接均对应一个双范畴余极限arxiv.org。通过这些余极限，开放系统的组合具有了泛性质（如并行组合是范畴内“最自由”的组合）。总计而言，双范畴层面的余极限概念在诸多应用中扮演关键角色：从在范畴间粘合信息（collage），到在形式范畴论中定义广义极限，再到在计算系统中描述规则合成与系统拼接，它提供了一种统一的高层语言，使我们能够将 策略组合、调度控制 等抽象为范畴结构中的态射来直接处理。这预示着，在未来的 DSL 设计与语义分析中，我们可以运用范畴论工具更自然地操纵和推理复杂系统的策略和逻辑link.springer.comarxiv.org。

参考文献：

• Yuto Kawase. Double categories of profunctors. arXiv preprint arXiv:2504.11099, 2025arxiv.org.

• Michael Shulman. Framed bicategories and monoidal fibrations. Theory Appl. Categ. 20: 650–738, 2008cl.cam.ac.uk.

• Patrick Schultz. Regular and exact (virtual) double categories. arXiv:1505.00712, 2015arxiv.org.

• Keisuke Hoshino, Hayato Nasu. Double categories of relations relative to factorisation systems. Applied Categorical Structures 33(2), 2025arxiv.org.

• Michael Lambert. Double Categories of Relations. arXiv:2107.07621, 2021.

• Seerp Roald Koudenburg. Formal category theory in augmented virtual double categories. Theory Appl. Categ. 41: 288–413, 2024.

• Meseguer, Montanari. Mapping tile logic into rewriting logic. In WADT’97, LNCS 1376, 1998link.springer.com.

• Gadducci, Montanari. Tile logic: theory and applications, 2000link.springer.com.

• Kenny Courser. Open Systems: A Double Categorical Perspective. PhD Thesis, U. Cambridge, 2020arxiv.org.

• Schultz, Spivak, Vasilakopoulou, Wisnesky. Algebraic databases. arXiv:1602.03501 (v3 2025)arxiv.orgarxiv.org.

• 等。 (以上列出文献的出版年份均在近20年内，以突出领域的相关进展。)