On the Theory of Structural Subtyping
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 <. C represents primitiv...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149974 |
| _version_ | 1826205502394073088 |
|---|---|
| author | Kuncak, Viktor Rinard, Martin |
| author_facet | Kuncak, Viktor Rinard, Martin |
| author_sort | Kuncak, Viktor |
| collection | MIT |
| description | 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 <. C represents primitive types; < 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. This result implies the decidability of the first-order theory of structural subtyping of non-recursive types. Our decision procedure is based on quantifier elimination and makes use of quantifier elimination for term algebras and Feferman-Vaught construction for products of decidable structures. We also explore connections between the theory of structural subtyping of recursive types and monadic second-order theory of tree-like structures. In particular, we give an embedding of the monadic second-order theory of infinite binary tree into the first-order theory of structural subtyping of recursive types. |
| first_indexed | 2024-09-23T13:14:23Z |
| id | mit-1721.1/149974 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T13:14:23Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1499742023-03-30T03:40:03Z On the Theory of Structural Subtyping Kuncak, Viktor Rinard, Martin 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 <. C represents primitive types; < 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. This result implies the decidability of the first-order theory of structural subtyping of non-recursive types. Our decision procedure is based on quantifier elimination and makes use of quantifier elimination for term algebras and Feferman-Vaught construction for products of decidable structures. We also explore connections between the theory of structural subtyping of recursive types and monadic second-order theory of tree-like structures. In particular, we give an embedding of the monadic second-order theory of infinite binary tree into the first-order theory of structural subtyping of recursive types. 2023-03-29T15:36:43Z 2023-03-29T15:36:43Z 2003-01 https://hdl.handle.net/1721.1/149974 MIT-LCS-TR-879 application/pdf |
| spellingShingle | Kuncak, Viktor Rinard, Martin On the Theory of Structural Subtyping |
| title | On the Theory of Structural Subtyping |
| title_full | On the Theory of Structural Subtyping |
| title_fullStr | On the Theory of Structural Subtyping |
| title_full_unstemmed | On the Theory of Structural Subtyping |
| title_short | On the Theory of Structural Subtyping |
| title_sort | on the theory of structural subtyping |
| url | https://hdl.handle.net/1721.1/149974 |
| work_keys_str_mv | AT kuncakviktor onthetheoryofstructuralsubtyping AT rinardmartin onthetheoryofstructuralsubtyping |