On the Theory of Structural Subtyping

paper ps   
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 <=. C represents primitive types; <= 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.

Citation

Viktor Kuncak and Martin Rinard. On the theory of structural subtyping. Technical Report 879, MIT LCS, 2003. Technical report version of [18].

BibTex Entry

@techreport{KuncakRinard03TheoryStructuralSubtyping,
  author = {Viktor Kuncak and Martin Rinard},
  title = {On the Theory of Structural Subtyping},
  institution = {MIT LCS},
  number = 879,
  year = 2003,
  url = {http://arxiv.org/abs/cs.LO/0408015},
  note = {Technical report version of 
          \cite{KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable}},
  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
$\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.
}
}