





















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.
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。