| 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.
|