论 ECC 中主类型的存在性及累积关系的良基性
计算机科学中的逻辑
2021-05-12 v4
摘要
当我们研究一个类型系统时，若能针对某种层级结构确立类型或项的良基性，则大有裨益，扩展构造演算（称为 ，在 [Luo,1994] 中被全面定义与研究）亦不例外。然而，在一种非常自然的层级关系（[Luo,1994] 中称为累积关系）下，该层级的良基性一般并不成立。本文中，我们证明若将累积关系限制于以下两类自然项族之一，则其是良基的：\begin{enumerate} \item 有效上下文中的类型 \item 具有范式（normal form）的项 \end{enumerate} 此外，我们独立给出了 中主类型存在性的证明，因其在有效上下文中累积关系良基性的证明中被用到，尽管该存在性常借助层级的良基性来证明，若采用那种方式会使我们的论证循环。
引用
@article{arxiv.2009.03486,
title = {On principal types and well-foundedness of the cummulativity relation in ECC},
author = {Eitetsu Ken and Masaki Natori and Kenji Tojo and Kazuki Watanabe},
journal= {arXiv preprint arXiv:2009.03486},
year = {2021}
}
备注
14 pages, no figures, the title changed, the historical remarks modified, the results unchanged, the e-mail addresses added