paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Van Kampen Colimits and Path Uniqueness

Van Kampen 余极限与路径唯一性
LMCS vol.Volume 14, Issue 22018匹配度 1/10 · 该论文属于纯范畴论与形式语义领域,研究 presheaf topoi 中 Van Kampen 性质的可判定条件和路径唯一性结构,与用户关注的 PL/AI 交叉、静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接关联。虽然涉及形式语义和 DSL/建模,但未触及用户当前核心研究问题。引用 1 inbox
Harald König, Uwe Wolter
crossref: 2026-09-10

AI 速览

一句话:给出 presheaf 拓扑斯中 Van Kampen 性质的充要且可高效判定条件,并揭示其路径唯一性结构特征。

本文关注软件工程模型-实例模式中基于纤维语义的模型组合问题。软件模型常可形式化为 presheaf 拓扑斯中的对象,多模型建模需要构造模型的余极限,分解则由拉回给出;组合性要求这些操作精确交互,即相关图表满足 Van Kampen 性质。然而按定义直接算法检查 Van Kampen 性质通常不可行。作者在 presheaf 拓扑斯中给出一个必要且充分、可高效检查的条件:它基于构成模型余极限余锥的定义同余类中路径状结构的唯一性。该结果补充了 Heindel 与 Sobociński 的“Van Kampen 是泛性质”命题,表明 Van Kampen 性质还体现 presheaf 基础上的结构唯一性特征。

问题
如何为 presheaf 拓扑斯中的模型组合与多模型建模,找到可算法化检查 Van Kampen 性质的判据?
方法
从纤维语义与 presheaf 拓扑斯出发,分析余极限余锥的定义同余类,提出基于路径状结构唯一性的充要条件。
评估
以理论证明建立该条件的必要性与充分性,并论证其可高效检查;摘要未报告实现或实验评估。
原文摘要(Abstract)

Fibred semantics is the foundation of the model-instance pattern of software engineering. Software models can often be formalized as objects of presheaf topoi, i.e, categories of objects that can be represented as algebras as well as coalgebras, e.g., the category of directed graphs. Multimodeling requires to construct colimits of models, decomposition is given by pullback. Compositionality requires an exact interplay of these operations, i.e., diagrams must enjoy the Van Kampen property. However, checking the validity of the Van Kampen property algorithmically based on its definition is often impossible. In this paper we state a necessary and sufficient yet efficiently checkable condition for the Van Kampen property to hold in presheaf topoi. It is based on a uniqueness property of path-like structures within the defining congruence classes that make up the colimiting cocone of the models. We thus add to the statement "Being Van Kampen is a Universal Property" by Heindel and Soboci\'{n}ski the fact that the Van Kampen property reveals a presheaf-based structural uniqueness feature.

链接与引用

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

BibTeX
@article{paperbot412,
  title = {Van Kampen Colimits and Path Uniqueness},
  author = {Harald König and Uwe Wolter},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 2},
  year = {2018},
  doi = {10.23638/lmcs-14(2:5)2018}
}