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

• Type: Conference
• Year: 2003
• Where: LICS
• Authors: Viktor Kuncak, Martin C. Rinard
• Keywords: Computer Science, LICS 2003, Non-recursive Types, Structural Subtyping, first-order Theory