paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The language of Stratified Sets is confluent and strongly normalising

分层集合语言具有合流性与强规范化性
LMCS vol.Volume 14, Issue 22018匹配度 1/10 · 该论文研究分层集合语言的合流与强规范化，属于形式语义与证明工程，未涉及用户核心关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析。引用 1 inbox
Murdoch J. Gabbay
定理证明与证明工程形式语义
crossref: 2026-09-10

AI 速览

一句话：证明分层集合语言的语法构成名义代数，且分层性/可分层性蕴含相应于β-转换的重写的合流与强规范化。

本文研究分层集合语言（含 ∈ 与分层条件的一阶逻辑，出现在 TST、TZT 以及以可分层性替代分层性的 Quine NF 中）的元理论性质。作者说明该语言的语法可构成处理替换的名义代数（nominal algebra），并分析对应于 β-转换的自然重写关系。关键结果是：分层性与可分层性都能保证该重写系统具有合流性（confluence）和强规范化（strong normalisation）。这为 TST、TZT 与 NF 中相关语言提供统一的语法与归约性质，说明其替换结构适合用名义代数刻画，且归约行为具有良好规范形式。

问题
分层集合语言（如 TST、TZT 与 Quine NF 所用语言）的替换结构与对应 β-转换的归约性质尚需统一刻画。
方法
将该语言语法形式化为名义代数（nominal algebra）以处理替换，并研究在分层/可分层条件下的重写系统。
评估
通过数学证明说明分层性与可分层性分别蕴含该重写系统的合流性与强规范化；属于理论证明，无实验评估。
原文摘要（Abstract）

We study the properties of the language of Stratified Sets (first-order logic with $\in$ and a stratification condition) as used in TST, TZT, and (with stratifiability instead of stratification) in Quine's NF. We find that the syntax forms a nominal algebra for substitution and that stratification and stratifiability imply confluence and strong normalisation under rewrites corresponding naturally to $\beta$-conversion.Comment: arXiv admin note: text overlap with arXiv:1406.4060

链接与引用

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

BibTeX 
@article{paperbot402,
  title = {The language of Stratified Sets is confluent and strongly normalising},
  author = {Murdoch J. Gabbay},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 2},
  year = {2018},
  doi = {10.23638/lmcs-14(2:12)2018}
}