On the Theory of Structural Subtyping

Abstract

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 <. C represents primitive types; < 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. This result implies the decidability of the first-order theory of structural subtyping of non-recursive types. Our decision procedure is based on quantifier elimination and makes use of quantifier elimination for term algebras and Feferman-Vaught construction for products of decidable structures. We also explore connections between the theory of structural subtyping of recursive types and monadic second-order theory of tree-like structures. In particular, we give an embedding of the monadic second-order theory of infinite binary tree into the first-order theory of structural subtyping of recursive types.