On Spatial Conjunction as Second-Order Logic
Spatial conjunction is a powerful construct for reasoning about dynamically allocateddata structures, as well as concurrent, distributed and mobile computation. Whileresearchers have identified many uses of spatial conjunction, its precise expressive powercompared to traditional logical constructs w...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30498 |
| _version_ | 1826207483568324608 |
|---|---|
| author | Kuncak, Viktor Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Kuncak, Viktor Rinard, Martin |
| author_sort | Kuncak, Viktor |
| collection | MIT |
| description | Spatial conjunction is a powerful construct for reasoning about dynamically allocateddata structures, as well as concurrent, distributed and mobile computation. Whileresearchers have identified many uses of spatial conjunction, its precise expressive powercompared to traditional logical constructs was not previously known.In this paper we establish the expressive power of spatial conjunction. We construct anembedding from first-order logic with spatial conjunction into second-order logic, and moresurprisingly, an embedding from full second order logic into first-order logic with spatialconjunction. These embeddings show that the satisfiability of formulas in first-order logicwith spatial conjunction is equivalent to the satisfiability of formulas in second-order logic.These results explain the great expressive power of spatial conjunction and can be usedto show that adding unrestricted spatial conjunction to a decidable logic leads to an undecidablelogic. As one example, we show that adding unrestricted spatial conjunction totwo-variable logic leads to undecidability.On the side of decidability, the embedding into second-order logic immediately implies thedecidability of first-order logic with a form of spatial conjunction over trees. The embeddinginto spatial conjunction also has useful consequences: because a restricted form of spatialconjunction in two-variable logic preserves decidability, we obtain that a correspondinglyrestricted form of second-order quantification in two-variable logic is decidable. The resultinglanguage generalizes the first-order theory of boolean algebra over sets and is useful inreasoning about the contents of data structures in object-oriented languages. |
| first_indexed | 2024-09-23T13:50:38Z |
| id | mit-1721.1/30498 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T13:50:38Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/304982019-04-11T06:23:34Z On Spatial Conjunction as Second-Order Logic Kuncak, Viktor Rinard, Martin Computer Architecture Spatial conjunction is a powerful construct for reasoning about dynamically allocateddata structures, as well as concurrent, distributed and mobile computation. Whileresearchers have identified many uses of spatial conjunction, its precise expressive powercompared to traditional logical constructs was not previously known.In this paper we establish the expressive power of spatial conjunction. We construct anembedding from first-order logic with spatial conjunction into second-order logic, and moresurprisingly, an embedding from full second order logic into first-order logic with spatialconjunction. These embeddings show that the satisfiability of formulas in first-order logicwith spatial conjunction is equivalent to the satisfiability of formulas in second-order logic.These results explain the great expressive power of spatial conjunction and can be usedto show that adding unrestricted spatial conjunction to a decidable logic leads to an undecidablelogic. As one example, we show that adding unrestricted spatial conjunction totwo-variable logic leads to undecidability.On the side of decidability, the embedding into second-order logic immediately implies thedecidability of first-order logic with a form of spatial conjunction over trees. The embeddinginto spatial conjunction also has useful consequences: because a restricted form of spatialconjunction in two-variable logic preserves decidability, we obtain that a correspondinglyrestricted form of second-order quantification in two-variable logic is decidable. The resultinglanguage generalizes the first-order theory of boolean algebra over sets and is useful inreasoning about the contents of data structures in object-oriented languages. 2005-12-22T02:14:54Z 2005-12-22T02:14:54Z 2004-10-25 MIT-CSAIL-TR-2004-067 MIT-LCS-TR-970 http://hdl.handle.net/1721.1/30498 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 16 p. 15950544 bytes 692945 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Kuncak, Viktor Rinard, Martin On Spatial Conjunction as Second-Order Logic |
| title | On Spatial Conjunction as Second-Order Logic |
| title_full | On Spatial Conjunction as Second-Order Logic |
| title_fullStr | On Spatial Conjunction as Second-Order Logic |
| title_full_unstemmed | On Spatial Conjunction as Second-Order Logic |
| title_short | On Spatial Conjunction as Second-Order Logic |
| title_sort | on spatial conjunction as second order logic |
| url | http://hdl.handle.net/1721.1/30498 |
| work_keys_str_mv | AT kuncakviktor onspatialconjunctionassecondorderlogic AT rinardmartin onspatialconjunctionassecondorderlogic |