Church-Style和Curry-Style子类型的关系
Relating Church-Style and Curry-Style Subtyping
摘要：
具有高阶子类型或单例类型的类型论是变量的计算规则受上下文中的类型信息影响的系统的示例。这些系统的一个复杂之处是，在上下文中声明的边界不能很好地与完整性或终止性的逻辑关系证明交互。本文对F-Omega-Sub的类型语法提出了一种自然的修改，将变量的绑定添加到变量类型构造函数中，从而将变量的计算行为与上下文分离。F-Omega-Sub中的子类型算法可以在没有上下文或种类信息的类型上给出。因此，元理论遵循了上下文中没有计算信息的类型系统的一般方法，包括一个简单的逻辑关系定义，而没有上下文的Kripke风格索引。这种新的表示系统被证明是等价于传统的表示没有界限的变量类型构造函数。
英文摘要：
Type theories with higher-order subtyping or singleton types are examples of systems where computation rules for variables are affected by type information in the context. A complication for these systems is that bounds declared in the context do not interact well with the logical relation proof of completeness or termination. This paper proposes a natural modification to the type syntax for F-Omega-Sub, adding variable's bound to the variable type constructor, thereby separating the computational behavior of the variable from the context. The algorithm for subtyping in F-Omega-Sub can then be given on types without context or kind information. As a consequence, the metatheory follows the general approach for type systems without computational information in the context, including a simple logical relation definition without Kripke-style indexing by context. This new presentation of the system is shown to be equivalent to the traditional presentation without bounds on the variable type constructor.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
