On the Theory of Structural Subtyping

Simple item page
dc.creatorKuncak, Viktor
dc.creatorRinard, Martin
dc.date2004-08-05
dc.date.accessioned2026-07-07T03:21:38Z
dc.date.available2026-07-07T03:21:38Z
dc.descriptionWe show that the first-order theory of structural subtyping of non-recursive types is decidable. Let $Σ$ 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 $Σ$-term-power of $C$, which generalizes the structure arising in structural subtyping. The domain of the $Σ$-term-power of $C$ is the set of $Σ$-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 $Σ$-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.
dc.description51 page. A version appeared in LICS 2003
dc.identifierhttps://arxiv.org/abs/cs/0408015
dc.identifierhttp://arxiv.org/abs/cs/0408015
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/32275
dc.subjectLogic in Computer Science
dc.subjectProgramming Languages
dc.subjectSoftware Engineering
dc.subjectD.2.4; D.3.1; D.3.3; F.3.1; F.3.2; F.4.1
dc.titleOn the Theory of Structural Subtyping
dc.typetext

Files

Collections

arXiv