paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Extending set functors to generalised metric spaces

将集合函子扩展为广义度量空间
LMCS vol.Volume 15, Issue 12019匹配度 2/10 · 该论文属于纯范畴论/形式语义,研究集合自函子到广义度量空间的扩展、左Kan扩展与终余代数,与用户核心关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析均无直接关联。仅作为程序语义的理论基础可能与形式化验证有极边缘联系,但完全不涉及用户列出的具体问题或LLM交叉方向。引用 2 inbox
Adriana Balan, Alexander Kurz, Jiří Velebil
crossref: 2026-09-10

AI 速览

一句话:证明集合自函子可典范扩展为广义度量空间上的自函子,并用左 Kan 扩展计算实例与终余代数。

论文研究如何把集合上的类型构造子(自函子 T)提升到交换 quantale V 丰富的 V-cat,即广义度量空间与非扩张映射范畴。作者证明存在典范扩展 T_V,从而使同一递归域方程 X≅TX 可在集合与度量空间等不同范畴中求解,并通过 change of base 研究其终余代数之间的关系。数学核心是证明离散函子 D:Set→V-cat 是 V-cat-dense 且具有密度表示,由此可沿 D 计算左 Kan 扩展。该证明给出具体实例的显式计算方法,涵盖 Pompeiu-Hausdorff 度量并产生新例子。此为 CALCO 2015 论文扩展版,新增 2.4、3.3 节,共 57 页,被 LMCS 接收。

问题
如何把集合上的类型构造子(自函子)典范地扩展到广义度量空间范畴 V-cat,并比较同一递归域方程 X≅TX 在不同范畴中的终余代数解。
方法
通过证明从集合到 V-cat 的离散函子 D 是 V-cat-dense 且具有密度表示,作者利用沿 D 的左 Kan 扩展构造 T_V,并给出具体实例的显式计算。
评估
评估以范畴论证明和实例计算为主:验证扩展可覆盖 Pompeiu-Hausdorff 度量等已知构造并产生新例,同时分析 change of base 下终余代数之间的关系。
原文摘要(Abstract)

For a commutative quantale $\mathcal{V}$, the category $\mathcal{V}-cat$ can be perceived as a category of generalised metric spaces and non-expanding maps. We show that any type constructor $T$ (formalised as an endofunctor on sets) can be extended in a canonical way to a type constructor $T_{\mathcal{V}}$ on $\mathcal{V}-cat$. The proof yields methods of explicitly calculating the extension in concrete examples, which cover well-known notions such as the Pompeiu-Hausdorff metric as well as new ones. Conceptually, this allows us to to solve the same recursive domain equation $X\cong TX$ in different categories (such as sets and metric spaces) and we study how their solutions (that is, the final coalgebras) are related via change of base. Mathematically, the heart of the matter is to show that, for any commutative quantale $\mathcal{V}$, the `discrete' functor $D:\mathsf{Set}\to \mathcal{V}-cat$ from sets to categories enriched over $\mathcal{V}$ is $\mathcal{V}-cat$-dense and has a density presentation that allows us to compute left-Kan extensions along $D$.Comment: 57 pages; extended version of the paper presented at CALCO 2015; accepted for publication in LMCS; Sections 2.4 and 3.3 were added

链接与引用

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

BibTeX
@article{paperbot834,
  title = {Extending set functors to generalised metric spaces},
  author = {Adriana Balan and Alexander Kurz and Jiří Velebil},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 15, Issue 1},
  year = {2019},
  doi = {10.23638/lmcs-15(1:5)2019}
}