Viktor Kuncak and Martin Rinard. On the theory of structural subtyping. Technical Report 879, MIT LCS, 2003. Technical report version of [18].

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.

[ bib | http ] Back