带有λ-类型λ表达式的扩展类型系统
摘要：扩展类型系统的lambda类型表达式的系统d被提出。它与来源于Automath项目的类型系统有关。d通过存在抽象运算符和命题运算符扩展了现有的lambda类型系统。eta-缩减扩展以使用经典否定的一部分规律来规范化否定表达式，因此d对于证明和公式都是正规化的，它们都被统一地处理为函数表达式。系统d使用一个常数au的自反类型公理，该常数无法为函数类型。证明了一些性质，包括合敛性，主题约简性，类型唯一性，强正规性和一致性。我们说明了当使用系统d时，由于其有限的逻辑强度，必须添加附加的公理来处理否定和数学结构的推导。
作者：Matthias Weber
论文ID：1803.10143
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22