一个相对逐渐的类型理论
摘要：渐进化归纳构造的演算（CIC）需要处理归一化、渐进性和与CIC的保守性之间微妙的张力。最近，已经提出了GCIC作为一个参数化的渐进类型理论，它包括三个变体，每个变体都牺牲其中一种属性。对于设计基于CIC的渐进证明助手来说，归一化和与CIC的保守性是关键，但需要解决与渐进性的张力。此外，还存在几个挑战：（1）在任何类型中存在两个通配符术语-错误术语和未知术语-可以对任何定理进行轻松证明，危及在证明助手中使用渐进类型理论; (2) 支持一般索引归纳族，尤其是相等性，是一个悬而未决的问题; (3) 到目前为止，关于渐进类型和渐进性的理论论述不支持处理规约过程中检测到的类型不匹配; (4) 精度和渐进性是外部概念，无法在渐进类型理论中进行推理。所有这些问题在CastCIC中原始地显示出来，CastCIC是用来定义GCIC的转换演算。在这项工作中，我们提出了一个名为GRIP的CastCIC扩展。GRIP是一个相对渐进的类型理论，解决了以上问题，具有内部精度和通用异常处理功能。GRIP包含一个被错误和未知术语填充的不纯（渐进）类型种类，以及一个用于一致推理渐进术语的纯（非渐进）严格命题种类。内部精度支持在GRIP中推理关于渐进性的问题，例如描述渐进异常处理术语，并支持渐进子集类型。我们使用Coq中建模的形式来开发GRIP的元理论，并在Agda中提供GRIP的原型实现。
作者：Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, ''Eric Tanter
论文ID：2209.00975
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-09-05