On the Theory of Structural Subtyping
<|reference_start|>On the Theory of Structural Subtyping: We show that the first-order theory of structural subtyping of non-recursive types is decidable. Let $\Sigma$ 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 $\Sigma$-term-power of $C$, which generalizes the structure arising in structural subtyping. The domain of the $\Sigma$-term-power of $C$ is the set of $\Sigma$-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 $\Sigma$-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.<|reference_end|>
@article{kuncak2004on,
    title={On the Theory of Structural Subtyping},
    author={Viktor Kuncak, Martin Rinard},
    journal={arXiv preprint arXiv:cs/0408015},
    year={2004},
    number={MIT CSAIL 879},
    archivePrefix={arXiv},
    eprint={cs/0408015},
    primaryClass={cs.LO cs.PL cs.SE}
}