list | abstracts | bib ]

Structural Subtyping of Non-Recursive Types is Decidable

paper pdf    paper ps   

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 Σ 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,
  localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03StructuralSubtypingNonRecursiveTypesDecidable.pdf}
}

list | abstracts | bib ]