list | abstracts | bib | http ]

On the Theory of Structural Subtyping

paper pdf    paper ps   

Abstract

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 [20].

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

list | abstracts | bib | http ]