paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the Nielsen-Schreier Theorem in Homotopy Type Theory

同伦类型论中的 Nielsen-Schreier 定理
LMCS vol.Volume 18, Issue 12022匹配度 1/10 · 该论文是纯 HoTT/类型论中的数学定理研究，主题为 Nielsen-Schreier 定理的形式化与构造性证明，与用户核心关注的静态分析、LLM/Agent 程序分析、浮点程序分析、贝叶斯程序分析均无直接关系；仅在“形式语义/类型系统”标签上与 PL 方向有很边缘的关联。引用 2 inbox
Andrew W Swan
类型系统形式语义
crossref: 2026-09-10

AI 速览

一句话：在 HoTT 中表述 Nielsen-Schreier 定理，构造性证明有限指数情形，并揭示全定理对选择公理的依赖及反例。

本文将群表述为带点连通 1-截断类型，在同伦类型论（HoTT）中重新表述 Nielsen-Schreier 定理，即自由群的子群自由。作者证明有限指数子群这一特殊情形可在构造性类型论中成立，而完整定理需要选择公理。进一步，论文给出一个布尔 ∞-拓扑斯，在其中该表述不成立；并证明一个更强的“未截断”版本在 HoTT 中可被证伪。该工作厘清了该定理的构造性内容、所依赖的公理以及与高阶结构之间的关系。

问题
研究 Nielsen-Schreier 定理（自由群的子群自由）在同伦类型论中的表述、构造性证明条件及其反例。
方法
将群视为带点连通 1-截断类型，在 HoTT 中形式化证明有限指数情形，并借助选择公理推导完整定理，同时用布尔 ∞-拓扑斯构造模型反例。
评估
通过构造性证明、模型反例以及证伪未截断版本，评估该定理在 HoTT 中的有效边界。
原文摘要（Abstract）

We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show the special case of finite index subgroups holds constructively and the full theorem follows from the axiom of choice. We give an example of a boolean infinity topos where our formulation of the theorem does not hold and show a stronger "untruncated" version of the theorem is provably false in homotopy type theory.

链接与引用

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

BibTeX 
@article{paperbot1737,
  title = {On the Nielsen-Schreier Theorem in Homotopy Type Theory},
  author = {Andrew W Swan},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 1},
  year = {2022},
  doi = {10.46298/lmcs-18(1:18)2022}
}