paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure

双范畴笛卡尔闭结构的相干性与求值规范化
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 1/10 · 该论文属于纯范畴论/形式语义,研究笛卡尔闭双范畴的相干性与normalisation-by-evaluation,不涉及LLM、Agent、静态分析、浮点程序分析或贝叶斯程序分析,与用户当前核心研究方向基本无关。引用 6 inbox
Marcelo Fiore, Philip Saville
crossref: 2026-09-12

AI 速览

一句话:给出笛卡尔闭双范畴相干性的两种证明,将高维结构构造归约到一维范畴论。

本文研究笛卡尔闭双范畴的相干性问题:在对象集合上自由生成的笛卡尔闭双范畴中,任意平行 1-胞之间的结构 2-胞至多只有一个。该结果把在任意笛卡尔闭双范畴中构造结构的困难归约为一维范畴论的层面。作者给出两种证明。第一种沿用经典的 Yoneda 引理方法;第二种则改造 Fiore 对简单类型 lambda 演算的 normalisation-by-evaluation 的范畴分析,将其提升到双范畴情形。作者指出,在构造好适当双范畴结构后,该论证并不比一维对应情形显著复杂,并为借助范畴语义工具进一步证明相干性开辟了道路。

问题
如何证明笛卡尔闭双范畴的相干性,即自由笛卡尔闭双范畴中任意平行 1-胞之间的结构 2-胞至多一个,从而简化在任意此类双范畴中构造结构的问题。
方法
第一种证明沿用 Yoneda 引理;第二种证明改造 Fiore 对简单类型 lambda 演算的 normalisation-by-evaluation 的范畴分析,并提升到双范畴设定。
评估
理论证明工作,无实验评估;通过两种独立证明及与一维对应情形的复杂度比较来支撑结论。
原文摘要(Abstract)

We present two proofs of coherence for cartesian closed bicategories. Precisely, we show that in the free cartesian closed bicategory on a set of objects there is at most one structural 2-cell between any parallel pair of 1-cells. We thereby reduce the difficulty of constructing structure in arbitrary cartesian closed bicategories to the level of 1-dimensional category theory. Our first proof follows a traditional approach using the Yoneda lemma. For the second proof, we adapt Fiore's categorical analysis of normalisation-by-evaluation for the simply-typed lambda calculus. Modulo the construction of suitable bicategorical structures, the argument is not significantly more complex than its 1-categorical counterpart. It also opens the way for further proofs of coherence using (adaptations of) tools from categorical semantics.

链接与引用

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

BibTeX
@inproceedings{paperbot5543,
  title = {Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure},
  author = {Marcelo Fiore and Philip Saville},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394769}
}