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.
}
}