LCS Publication Details
Publication Title: On the Theory of Structural Subtyping
Publication Author: Kuncak, Viktor
Additional Authors: Martin Rinard
LCS Document Number: MIT-LCS-TR-879
Publication Date: 1-20-2003
LCS Group: Computer Architecture
Additional URL:
Abstract:
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 structures. 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 MIT Document Services.