paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Impredicative Encodings of (Higher) Inductive Types

（高阶）归纳类型的非直谓编码
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 该论文属于类型论/同伦类型论的基础理论研究，讨论非直谓编码、η-等式与高阶归纳类型，与用户画像中 LLM/Agent 结合的静态分析、形式化验证、浮点程序分析或贝叶斯程序分析等核心方向没有直接关联；仅可作为 PL/形式化验证底层理论的间接背景。引用 17 inbox
Steve Awodey, Jonas Frey, Sam Speight
类型系统
crossref: 2026-09-12

AI 速览

一句话：提出用同伦类型论思想精化非直谓编码，使有限归纳类型恢复 η 等式与依赖消去，并扩展到部分高阶归纳类型。

在依赖类型论中，公理地引入非直谓宇宙可以像 System F 那样编码有限归纳类型，但这类编码不能满足相应的 η 等式，因此无法支持依赖消去子。为恢复 η 等式与依赖消去，本文借鉴同伦类型论中的思想，提出一种构造这些非直谓编码之精化（refinement）的方法。该方法不只是直接翻译归纳类型的通常编码，而是通过额外结构使编码具备正确的消去性质。作者进一步将方法扩展到某些高阶归纳类型，例如 1-truncation 和单位圆 S^1，给出它们的非直谓编码。该工作为在非直谓类型论中统一处理（高阶）归纳类型提供了理论构造，并阐明同伦类型论工具在编码问题上的作用。

问题
非直谓宇宙中 System F 风格编码虽能表示有限归纳类型，却缺失相应的 η 等式，进而无法支持依赖消去子。
方法
借助同伦类型论思想构造这些非直谓编码的精化，并推广到 1-truncation 与单位圆 S^1 等高阶归纳类型。
评估
摘要未报告实现或实验；评估主要是理论性的，通过给出精化构造并展示其可扩展到若干高阶归纳类型来验证方法。
原文摘要（Abstract）

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.

链接与引用

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

BibTeX 
@inproceedings{paperbot4381,
  title = {Impredicative Encodings of (Higher) Inductive Types},
  author = {Steve Awodey and Jonas Frey and Sam Speight},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209130}
}