On the Theory of Structural Subtyping

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. This result implies the decidability of the first-order theory of structural subtyping of non-recursive types. Our decision procedure is based on quantifier elimination and makes use of quantifier elimination for term algebras and Feferman-Vaught construction for products of decidable structures. We also explore connections between th...

• Type: Journal
• Year: 2004
• Where: CORR
• Authors: Viktor Kuncak, Martin C. Rinard
• Keywords: CORR 2004, Education, First-order Theory, Non-recursive Types, Structural Subtyping