Computer Science – Logic in Computer Science
Scientific paper
2004-08-05
Computer Science
Logic in Computer Science
51 page. A version appeared in LICS 2003
Scientific paper
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 $\leq$. $C$ represents primitive types; $\leq$ 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$. Our decision procedure makes use of quantifier elimination for term algebras and Feferman-Vaught theorem. Our result implies the decidability of the first-order theory of structural subtyping of non-recursive types.
Kuncak Viktor
Rinard Martin
No associations
LandOfFree
On the Theory of Structural Subtyping does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with On the Theory of Structural Subtyping, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the Theory of Structural Subtyping will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-410127