Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

LICS

2003

IEEE

2003

IEEE

We show that the ﬁrst-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 ﬁnite or inﬁnite 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 deﬁned by lifting operations of C to terms over C. We extend quantiﬁer elimination for term algebras and apply the Feferman-Vaught technique for quantiﬁer 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...

Related Content

Added |
05 Jul 2010 |

Updated |
05 Jul 2010 |

Type |
Conference |

Year |
2003 |

Where |
LICS |

Authors |
Viktor Kuncak, Martin C. Rinard |

Comments (0)