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.


翻译:当我们调查一种类型体系时,如果我们能够确定某等级体系中类型或术语的充足性,那将是有益的,而建筑工程的扩展计算(在[Luo,1994] 中定义和全面研究的称为$ECC$,在[Luo,1994] 中称为$ECC$)也不例外。然而,在非常自然的等级关系(在[Luo,1994] 中称为累积性关系)下,等级体系的健全性一般不成立。在本条中,我们表明,如果累积性关系限于以下两个自然术语类别中的一个:\ begin{numberte}\ 项类型在有效背景下具有正常形式的项目术语\ end{uncutate},那么我们独立地证明主要类别存在于$ECC$,因为它用于证明累积性关系在有效背景下有充分根据,尽管常常通过利用等级的充足性来证明,从而证明这种累积性关系是有充分的,如果通过采纳的话,我们的论点会循环。

0
下载
关闭预览

相关内容

专知会员服务
50+阅读 · 2020年12月14日
知识图谱在可解释人工智能中的作用,附81页ppt
专知会员服务
136+阅读 · 2019年11月11日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
186+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
计算机类 | LICS 2019等国际会议信息7条
Call4Papers
3+阅读 · 2018年12月17日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
计算机视觉近一年进展综述
机器学习研究会
8+阅读 · 2017年11月25日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Capsule Networks解析
机器学习研究会
10+阅读 · 2017年11月12日
【今日新增】IEEE Trans.专刊截稿信息8条
Call4Papers
7+阅读 · 2017年6月29日
Arxiv
0+阅读 · 2021年6月26日
Arxiv
6+阅读 · 2018年3月31日
VIP会员
相关VIP内容
专知会员服务
50+阅读 · 2020年12月14日
知识图谱在可解释人工智能中的作用,附81页ppt
专知会员服务
136+阅读 · 2019年11月11日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
186+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
相关资讯
计算机 | 国际会议信息5条
Call4Papers
3+阅读 · 2019年7月3日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
计算机类 | LICS 2019等国际会议信息7条
Call4Papers
3+阅读 · 2018年12月17日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
计算机视觉近一年进展综述
机器学习研究会
8+阅读 · 2017年11月25日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Capsule Networks解析
机器学习研究会
10+阅读 · 2017年11月12日
【今日新增】IEEE Trans.专刊截稿信息8条
Call4Papers
7+阅读 · 2017年6月29日
Top
微信扫码咨询专知VIP会员