||On the Theory of Structural Subtyping
|LCS Document Number:
|We show that the first-order theory of structural subtyping
of non-recursive types is decidable.
Let Sigma 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 Sigma-term-power of C,
which generalizes the structure arising in structural
subtyping. The domain of the Sigma-term-power of C is the
set of Sigma-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 Sigma-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
We also explore connections between the theory of structural
subtyping of recursive types and monadic second-order theory
of tree-like structures. In particular, we give an
embedding of the monadic second-order theory of infinite
binary tree into the first-order theory of structural
subtyping of recursive types.
|To obtain this publication:
To purchase a printed copy of this publication please contact