重新审视可判定的有界量化，经由自然性
Revisiting Decidable Bounded Quantification, via Dinaturality
AI总结：
通过语义解释和自然性，将有界量化的两种规则统一于单一类型系统，使其具有最小类型性质，并证明相关片段的类型检查可判定，包括System Fsubtop对β-正规项的类型检查。
摘要：
我们使用语义解释来研究定义一个富有表现力但可判定的、带有有界量化的类型系统的问题。在广泛研究的System Fsub中，类型检查是不可判定的，这归因于其不可判定的子类型关系，而罪魁祸首是处理有界量化子类型的规则。已有研究提出了该规则的较弱版本，使得子类型关系可判定。由此产生的类型系统中，一个（Kernel Fsub）缺乏表现力，另一个（System Fsubtop）缺乏最小类型性质，因此没有明显的类型检查算法。我们将这些规则视为定义了不同形式的有界量化：一种用于解释类型变量抽象，另一种用于类型实例化。通过基于无界量化对两者给出语义解释，并利用类型实例化关于子类型的自然性，我们证明了它们可以在单一类型系统中共存。该类型系统确实具有最小类型性质，因此具有简单的类型检查过程。我们考虑这个统一类型系统中仅包含一种有界量词形式的类型的片段。其中一个片段等价于Kernel Fsub，而另一个片段能够对严格更多的项进行类型化，但仅对相同的β-正规项集合进行类型化。我们证明了该片段的类型检查可判定性，从而也证明了System Fsubtop对β-正规项的类型检查可判定性。
英文摘要：
We use a semantic interpretation to investigate the problem of defining an expressive but decidable type system with bounded quantification. Typechecking in the widely studied System Fsub is undecidable thanks to an undecidable subtyping relation, for which the culprit is the rule for subtyping bounded quantification. Weaker versions of this rule, allowing decidable subtyping, have been proposed. One of the resulting type systems (Kernel Fsub) lacks expressiveness, another (System Fsubtop) lacks the minimal typing property and thus has no evident typechecking algorithm. We consider these rules as defining distinct forms of bounded quantification, one for interpreting type variable abstraction, and the other for type instantiation. By giving a semantic interpretation for both in terms of unbounded quantification, using the dinaturality of type instantiation with respect to subsumption, we show that they can coexist within a single type system. This does have the minimal typing property and thus a simple typechecking procedure. We consider the fragments of this unified type system over types which contain only one form of bounded quantifier. One of these is equivalent to Kernel Fsub, while the other can type strictly more terms than System Fsubtop but the same set of beta-normal terms. We show decidability of typechecking for this fragment, and thus for System Fsubtop typechecking of beta-normal terms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
