[ 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* 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*_{P} the family of their
Σ-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.

### 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 ]