paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Natural numbers from integers

从整数类型构造自然数类型
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 1/10 · 该论文属于同伦类型论的纯理论构造，讨论如何从整数类型构造自然数类型，与用户关注的静态分析、程序分析、LLM/Agent 交叉、浮点程序分析、贝叶斯程序分析等方向没有直接关联。虽然涉及类型系统，但并非程序分析或形式化验证的应用研究。引用 0 inbox
Christian Sattler, David Wärn
类型系统
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：仅用 Σ、Id、Π 与带大消去的二元素类型，从整数类型构造出自然数类型。

在同伦类型论（HoTT）中，自然数类型可视为由一元素与一自同态自由生成，整数类型则由一元素与一自同构自由生成。本文的核心是从整数类型出发构造自然数类型，且只使用依赖和类型、同一类型、外延依赖积，以及带大消去的二元素类型。由此得到推论：仅含 Σ、Id、Π 与带下降（descent）的有限余极限、不含宇宙的同伦类型论也允许自然数类型。作者指出该构造改进并简化了 Rose 的已有结果。

问题
在较弱的同伦类型论系统中，自然数类型是否可由整数类型导出？
方法
利用依赖和、同一类型、外延依赖积和带大消去的二元素类型，从整数类型构造自然数类型。
评估
给出构造性证明及其关于 Σ、Id、Π 与有限余极限的推论，并说明相比 Rose 结果的改进与简化。
原文摘要（Abstract）

In homotopy type theory, a natural number type is freely generated by an element and an endomorphism. Similarly, an integer type is freely generated by an element and an automorphism. Using only dependent sums, identity types, extensional dependent products, and a type of two elements with large elimination, we construct a natural number type from an integer type. As a corollary, homotopy type theory with only Σ, Id, Π, and finite colimits with descent (and no universes) admits a natural number type. This improves and simplifies a result by Rose.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@inproceedings{abs-2405-18388,
  title = {Natural numbers from integers},
  author = {Christian Sattler and David Wärn},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662129}
}