Publication Title: 
On the Theory of Structural Subtyping 
Publication Author: 
Kuncak, Viktor 
Additional Authors: 
Martin Rinard 
LCS Document Number: 
MITLCSTR879 
Publication Date: 
1202003 
LCS Group: 
Computer Architecture 
Additional URL: 

Abstract: 
We show that the firstorder theory of structural subtyping
of nonrecursive 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 Sigmatermpower of C,
which generalizes the structure arising in structural
subtyping. The domain of the Sigmatermpower of C is the
set of Sigmaterms over the set of elements of C.
We show that the decidability of the firstorder theory of
C implies the decidability of the firstorder theory of
the Sigmatermpower of C. This result implies the
decidability of the firstorder theory of structural
subtyping of nonrecursive types.
Our decision procedure is based on quantifier elimination
and makes use of quantifier elimination for term algebras
and FefermanVaught construction for products of decidable
structures.
We also explore connections between the theory of structural
subtyping of recursive types and monadic secondorder theory
of treelike structures. In particular, we give an
embedding of the monadic secondorder theory of infinite
binary tree into the firstorder theory of structural
subtyping of recursive types. 
To obtain this publication: 

To purchase a printed copy of this publication please contact
MIT
Document Services.
