Structural Subtyping of Non-Recursive Types is Decidable

10 years 3 hour ago
Structural Subtyping of Non-Recursive Types is Decidable
We show that the first-order theory of structural subtyping of non-recursive types is decidable, as a consequence of a more general result on the decidability of term powers of decidable theories. Let Σ be a language consisting of function symbols and let C (with a finite or infinite domain C) be an L-structure where L is a language consisting of relation symbols. We introduce the notion of Σ-term-power of the structure C, denoted PΣ(C). The domain of PΣ(C) is the set of Σ-terms over the set C. PΣ(C) has one term algebra operation for each f ∈ Σ, and one relation for each r ∈ L defined by lifting operations of C to terms over C. We extend quantifier elimination for term algebras and apply the Feferman-Vaught technique for quantifier elimination in products to obtain the following result. Let K be a family of L-structures and KP the family of their Σ-termpowers. Then the validity of any closed formula F on KP can be effectively reduced to the validity of some closed f...
Viktor Kuncak, Martin C. Rinard
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where LICS
Authors Viktor Kuncak, Martin C. Rinard
Comments (0)