重访可判定有界量化，通过Dinaturality
摘要：使用语义解释来研究定义具有有限定量但可决定的表达能力的类型系统的问题。在广泛研究的System Fsub中，类型检查是不可决定的，归咎于不可决定的子类型关系，其中被限定的定量子类型的子类型规则是罪魁祸首。已经提出了一种允许可决定子类型的该规则的较弱版本。由此产生的其中一个类型系统（Kernel Fsub）缺乏表达能力，另一个类型系统（System Fsubtop）缺乏最小类型化特性，因此没有明显的类型检查算法。 我们将这些规则视为定义有限量化的不同形式，一种用于解释类型变量抽象，另一种用于类型实例化。通过在不受限量化范围内给出对两者的语义解释，使用类型实例化与包含关系的双自然性，我们证明它们可以在一个单一的类型系统中共存。这个系统具有最小类型化特性，因此有一个简单的类型检查过程。 我们考虑这个统一类型系统的片段，其中包含只有一种形式的有限定量子的类型。其中之一等价于Kernel Fsub，而另一个可以给出比System Fsubtop更多的项的类型，但是给出相同的正规项集合。我们证明了这个片段的类型检查的可决定性，从而为System Fsubtop的类型检查的正规项提供了可决定性。
作者：James Laird
论文ID：2212.04882
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22