纯类型系统中的弱规范性与强规范性
Weak and strong normalization in pure type systems
OpenAI 数学仓库收录的研究手稿。展开查看英文摘要，或标记后让我进一步解释。
具体内容
该稿件研究纯类型系统中的β归约规范性。作者声称证明了每个弱β规范的纯类型系统都是强β规范的，其中两种性质都量化所有合法上下文中的合法表达式，归约作用于类型标注内部，且不需要功能性假设。摘要称这解决了β-Barendregt–Geuvers–Klop猜想。若成立，这将在不假设功能性的条件下统一纯类型系统的弱与强规范性。
- 研究对象为纯类型系统中所有合法表达式的β弱规范性与强规范性
- 作者声称弱β规范蕴含强β规范，且无需功能性假设
- 归约作用于类型标注内部，摘要称解决Barendregt–Geuvers–Klop猜想
AI 产生的研究手稿；收录不表示已完成独立审查或同行评议。
英文原始摘要
We prove that every weakly β-normalizing pure type system is strongly β-normalizing. Both properties quantify over all legal expressions in all valid contexts, and reduction acts inside type annotations. No functionality hypothesis is required. This resolves the β-Barendregt–Geuvers–Klop conjecture.
用户标记：未标记
固定编号：92b00dd495698221
原文来源