论文标题
关于ECC中关联关系的主要类型和良好的基础
On principal types and well-foundedness of the cummulativity relation in ECC
论文作者
论文摘要
当我们调查类型系统时，如果我们可以在某个层次结构方面建立类型或术语的良好的类型或术语，并且构造的扩展计算（称为$ ECC $，在[Luo，1994]中进行了全面定义和研究）是有帮助的。但是，在非常自然的层次结构关系下（称为[Luo，1994]中的累积关系），层次结构的良好基础并不一般。 在本文中，我们表明，如果累计关系仅限于以下两个自然术语之一： \开始{枚举} \在有效上下文中的项目类型 \具有正常表格的项目条款 \ end {枚举} 此外，我们给出了$ ECC $中主要类型的独立证明，因为它用于证明在有效背景下累积关系的良好基础的证明，尽管通常可以通过利用层次结构的良好基础来证明，这将使我们的论点循环通过，如果采用了。
When we investigate a type system, it is helpful if we can establish the well-foundedness of types or terms with respect to a certain hierarchy, and the Extended Calculus of Constructions (called $ECC$, defined and studied comprehensively in [Luo,1994]) is no exception. However, under a very natural hierarchy relation (called the cumulativity relation in [Luo,1994]), the well-foundedness of the hierarchy does not hold generally. In this article,we show that the cumulativity relation is well-founded if it is restricted to one of the following two natural families of terms: \begin{enumerate} \item types in a valid context \item terms having normal forms \end{enumerate} Also, we give an independent proof of the existence of principal types in $ECC$ since it is used in the proof of well-foundedness of cumulativity relation in a valid context although it is often proved by utilizing the well-foundedness of the hierarchy, which would make our argument circular if adopted.
