We show that the first-order theory of structural subtyping of non-recursive types is decidable, as a consequence of a more general result on the decidability of term powers of decidable theories. Let Σ be a language consisting of function symbols and let(with a finite or infinite domainCC) be anL-structure whereLis a language consisting of relation symbols. We introduce the notion of Σ-term-power of the structure, denotedCP_{Σ}(). The domain ofCP_{Σ}() is the set of Σ-terms over the setCC.P_{Σ}() has one term algebra operation for eachCfin Σ, and one relation for eachrinLdefined by lifting operations ofto terms overCC. We extend quantifier elimination for term algebras and apply the Feferman-Vaught technique for quantifier elimination in products to obtain the following result. LetKbe a family ofL-structures andK_{P}the family of their Σ-term-powers. Then the validity of any closed formulaFonK_{P}can be effectively reduced to the validity of some closed formulaq(F) onK. Our result implies the decidability of the first-order theory of structural subtyping of non-recursive types with covariant constructors, and the construction generalizes to contravariant constructors as well.

@inproceedings{KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable, author = {Viktor Kuncak and Martin Rinard}, title = {Structural Subtyping of Non-Recursive Types is Decidable}, booktitle = {Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS)}, publisher = {IEEE}, isbn = {0-7695-1884-2}, year = 2003, abstract = { We show that the first-order theory of structural subtyping of non-recursive types is decidable, as a consequence of a more general result on the decidability of term powers of decidable theories. Let $\Sigma$ be a language consisting of function symbols and let $\mathbf{C}$ (with a finite or infinite domain $C$) be an $L$-structure where $L$ is a language consisting of relation symbols. We introduce the notion of $\Sigma$-term-power of the structure $\mathbf{C}$, denoted $P_{\Sigma}(\mathbf{C})$. The domain of $P_{\Sigma}(\mathbf{C})$ is the set of $\Sigma$-terms over the set $C$. $P_{\Sigma}(\mathbf{C})$ has one term algebra operation for each $f \in \Sigma$, and one relation for each $r \in L$ defined by lifting operations of $\mathbf{C}$ to terms over $C$. We extend quantifier elimination for term algebras and apply the Feferman-Vaught technique for quantifier elimination in products to obtain the following result. Let $K$ be a family of $L$-structures and $K_P$ the family of their $\Sigma$-term-powers. Then the validity of any closed formula $F$ on $K_P$ can be effectively reduced to the validity of some closed formula $q(F)$ on $K$. Our result implies the decidability of the first-order theory of structural subtyping of non-recursive types with covariant constructors, and the construction generalizes to contravariant constructors as well. } }