Structural Subtyping of Non-Recursive Types is Decidable

paper ps   
We show that the first-order theory of structural subtyping of non-recursive types is decidable, as a consequence of a more general result on the decidability of term powers of decidable theories. Let Σ be a language consisting of function symbols and let C (with a finite or infinite domain C) be an L-structure where L is a language consisting of relation symbols. We introduce the notion of Σ-term-power of the structure C, denoted PΣ(C). The domain of PΣ(C) is the set of Σ-terms over the set C. PΣ(C) has one term algebra operation for each f in Σ, and one relation for each r inL defined by lifting operations of C to terms over C. We extend quantifier elimination for term algebras and apply the Feferman-Vaught technique for quantifier elimination in products to obtain the following result. Let K be a family of L-structures and KP the family of their Σ-term-powers. Then the validity of any closed formula F on KP can be effectively reduced to the validity of some closed formula q(F) on K. Our result implies the decidability of the first-order theory of structural subtyping of non-recursive types with covariant constructors, and the construction generalizes to contravariant constructors as well.

Citation

Viktor Kuncak and Martin Rinard. Structural subtyping of non-recursive types is decidable. In Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2003.

BibTex Entry

@inproceedings{KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable,
  author = {Viktor Kuncak and Martin Rinard},
  title = {Structural Subtyping of Non-Recursive Types is Decidable},
  booktitle = {Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS)},
  publisher = {IEEE},
  isbn = {0-7695-1884-2},
  year = 2003,
  abstract = {
We show that the first-order theory of structural subtyping
of non-recursive types is decidable, as a consequence of a
more general result on the decidability of term powers of
decidable theories.

Let $\Sigma$ be a language consisting of function symbols and let
$\mathbf{C}$ (with a finite or infinite domain $C$) be an
$L$-structure where $L$ is a language consisting of relation
symbols.  We introduce the notion of $\Sigma$-term-power
of the structure $\mathbf{C}$, denoted $P_{\Sigma}(\mathbf{C})$.  The domain
of $P_{\Sigma}(\mathbf{C})$ is the set of $\Sigma$-terms over the set $C$.
$P_{\Sigma}(\mathbf{C})$ has one term algebra operation for each $f \in
\Sigma$, and one relation for each $r \in L$ defined by lifting
operations of $\mathbf{C}$ to terms over $C$.

We extend quantifier elimination for term algebras and apply
the Feferman-Vaught technique for quantifier elimination in
products to obtain the following result.  Let $K$ be a family
of $L$-structures and $K_P$ the family of their
$\Sigma$-term-powers.  Then the validity of any closed
formula $F$ on $K_P$ can be effectively reduced to the
validity of some closed formula $q(F)$ on $K$.

Our result implies the decidability of the first-order
theory of structural subtyping of non-recursive types with
covariant constructors, and the construction generalizes to
contravariant constructors as well.
}
}