论结构子类型理论
On the Theory of Structural Subtyping
摘要：
我们证明了非递归类型的结构子类型的一阶理论是可判定的。设$Σ$是一种由函数符号（表示类型构造函数）组成的语言，$C$是关系语言$L$中包含二元关系$\leq$的可判定结构。$C$表示基本类型; $\leq$表示子类型排序。我们引入了$Σ$-$C$的项幂的概念，它概括了结构子类型中出现的结构。$C$的$Σ$ -项-幂的域是$C$的元素集合上的$Σ$ -项的集合。我们证明了$C$的一阶理论的可判定性意味着$C$的$Σ$ -项-幂的一阶理论的可判定性。我们的决策过程中使用的量词消去的项代数和Feferman-Vaught定理。我们的结果暗示了非递归类型的结构子类型的一阶理论的可判定性。
英文摘要：
We show that the first-order theory of structural subtyping of non-recursive types is decidable. Let $Σ$ be a language consisting of function symbols (representing type constructors) and $C$ a decidable structure in the relational language $L$ containing a binary relation $\leq$. $C$ represents primitive types; $\leq$ represents a subtype ordering. We introduce the notion of $Σ$-term-power of $C$, which generalizes the structure arising in structural subtyping. The domain of the $Σ$-term-power of $C$ is the set of $Σ$-terms over the set of elements of $C$. We show that the decidability of the first-order theory of $C$ implies the decidability of the first-order theory of the $Σ$-term-power of $C$. Our decision procedure makes use of quantifier elimination for term algebras and Feferman-Vaught theorem. Our result implies the decidability of the first-order theory of structural subtyping of non-recursive types.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
