F-有界量词和等递归类型的子类型（扩展版）
Subtyping for F-Bounded Quantifiers and Equirecursive Types (Extended Version)
摘要：
本文定义了绑定树的概念，为具有F-有界量词和等递归类型的二阶类型系统提供了一个合适的模型。它定义了一个正则绑定树的概念，它以正确的方式对应于一阶情况下的正则性概念。它定义了这些树的子类型的概念，并证明了子类型关系的各种属性。它定义了一个从类型到树的映射，并说明了类型会产生规则的绑定树。它提出了一组类型相等和子类型规则，并证明了它们的声音和完整的树解释。它定义了绑定树自动机的概念，以及这些自动机如何生成规则绑定树。给出了判定两个自动机的树何时处于子类型关系的多项式时间算法。
英文摘要：
This paper defines a notion of binding trees that provide a suitable model for second-order type systems with F-bounded quantifiers and equirecursive types. It defines a notion of regular binding trees that correspond in the right way to notions of regularity in the first-order case. It defines a notion of subtyping on these trees and proves various properties of the subtyping relation. It defines a mapping from types to trees and shows that types produce regular binding trees. It presents a set of type equality and subtyping rules, and proves them sound and complete with respect to the tree interpretation. It defines a notion of binding-tree automata and how these generate regular binding trees. It gives a polynomial-time algorithm for deciding when two automata's trees are in the subtyping relation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
