# IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

# Logic in Computer Science (LICS 2003)

## Paper: Structural Subtyping of Non-Recursive Types is Decidable (at LICS 2003)

Authors: Viktor Kuncak Martin C. Rinard

### 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 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 C, denoted P(C). The domain of P(C) is the set of \Sigma-terms over the set C. P(C) has one term algebra operation for each f \in \Sigma, and one relation for each r \in L 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 K the family of their \Sigma-term-powers. Then the validity of any closed formula F on K 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 co-variant constructors, and the construction generalizes to contravariant constructors as well.

### BibTeX

  @InProceedings{KuncakRinard-StructuralSubtyping,
author = 	 {Viktor Kuncak and Martin C. Rinard},
title = 	 {Structural Subtyping of Non-Recursive Types is Decidable},
booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
year =	 {2003},
month =	 {June},
pages =      {96--107},