On the Theory of Structural Subtyping

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.

Abstract licence: CC0

A person counts once a day per paper. We keep no cookie and no address: a reader is a hash that changes every day. Any month under five reads shows no number.