Document Open Access Logo

Spatial Existential Positive Logics for Hyperedge Replacement Grammars

Author Yoshiki Nakamura

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2022.30.pdf
  • Filesize: 0.9 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Existential positive logic
  • spatial logic
  • Kleene theorem

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We study a (first-order) spatial logic based on graphs of conjunctive queries for expressing (hyper-)graph languages. In this logic, each primitive positive (resp. existential positive) formula plays a role of an expression of a graph (resp. a finite language of graphs) modulo graph isomorphism. First, this paper presents a sound- and complete axiomatization for the equational theory of primitive/existential positive formulas under this spatial semantics. Second, we show Kleene theorems between this logic and hyperedge replacement grammars (HRGs), namely that over graphs, the class of existential positive first-order (resp. least fixpoint, transitive closure) formulas has the same expressive power as that of non-recursive (resp. all, linear) HRGs.

Cite As Get BibTex

Yoshiki Nakamura. Spatial Existential Positive Logics for Hyperedge Replacement Grammars. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.30

Author Details

Yoshiki Nakamura
  • Tokyo Institute of Technology, Japan

Funding

This work was supported by JSPS KAKENHI Grant Number JP21K13828.

Acknowledgements

We would like to thank the anonymous reviewers for their useful comments.

References

  1. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison-Wesley, 1995. Google Scholar
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/cbo9781139172752.
  3. Michel Bauderon and Bruno Courcelle. Graph expressions and graph rewritings. Mathematical Systems Theory, 20(1):83-127, 1987. URL: https://doi.org/10.1007/BF01692060.
  4. Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical Conjunctive Queries. In 27th EACSL Annual Conference on Computer Science Logic (CSL '18), volume 119, pages 13:1-13:23. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.13.
  5. Francis Bossut, Max Dauchet, and Bruno Warin. A Kleene Theorem for a Class of Planar Acyclic Graphs. Information and Computation, 117(2):251-265, 1995. URL: https://doi.org/10.1006/inco.1995.1043.
  6. Paul Brunet and Damien Pous. Petri automata. Logical Methods in Computer Science, 13(3), 2017. URL: https://doi.org/10.23638/LMCS-13(3:33)2017.
  7. Janusz A. Brzozowski and Edward J. McCluskey. Signal Flow Graph Techniques for Sequential Circuit State Diagrams. IEEE Transactions on Electronic Computers, EC-12(2):67-76, 1963. URL: https://doi.org/10.1109/PGEC.1963.263416.
  8. J. Richard Büchi. Weak Second-Order Arithmetic and Finite Automata. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 6(1-6):66-92, 1960. URL: https://doi.org/10.1002/malq.19600060105.
  9. J. Richard Büchi. On a Decision Method in Restricted Second Order Arithmetic. In International Congress on Logic, Methodology, and Philosophy of Science 1960, pages 1-11. Stanford University Press, 1962. Google Scholar
  10. Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. A Spatial Logic for Querying Graphs. In International Colloquium on Automata, Languages, and Programming (ICALP '02), pages 597-610. Springer Verlag, 2002. URL: https://doi.org/10.1007/3-540-45465-9_51.
  11. Ashok K. Chandra and Philip M. Merlin. Optimal implementation of conjunctive queries in relational data bases. In 9th annual ACM symposium on Theory of computing (STOC '77), pages 77-90. ACM Press, 1977. URL: https://doi.org/10.1145/800105.803397.
  12. Chandra Chekuri and Anand Rajaraman. Conjunctive query containment revisited. Theoretical Computer Science, 239(2):211-229, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00220-0.
  13. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications, 2007. URL: http://www.grappa.univ-lille3.fr/tata.
  14. Enric Cosme Llópez and Damien Pous. K4-free Graphs as a Free Algebra. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS '17), pages 76:1-76::14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.MFCS.2017.76.
  15. Bruno Courcelle and Joost Engelfriet. A Logical Characterization of the Sets of Hypergraphs Defined by Hyperedge Replacement Grammars. Mathematical Systems Theory, 28(6):515-552, 1995. Google Scholar
  16. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9780511977619.
  17. Werner Damm. The IO- and OI-hierarchies. Theoretical Computer Science, 20(2):95-207, 1982. URL: https://doi.org/10.1016/0304-3975(82)90009-3.
  18. Christian Doczkal and Damien Pous. Treewidth-Two Graphs as a Free Algebra. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS '18), volume 117, pages 60:1-60:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.60.
  19. Frank Drewes, Hans-Jörg Kreowski, and Annegret Habel. Hyperedge Replacement Graph Grammars. In Handbook of Graph Grammars and Computing by Graph Transformation, Volume 1: Foundations, chapter 2, pages 95-162. World Scientific, 1997. URL: https://doi.org/10.1142/9789812384720_0002.
  20. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer Monographs in Mathematics. Springer, 2 edition, 1995. URL: https://doi.org/10.1007/3-540-28788-4.
  21. Calvin C. Elgot. Decision Problems of Finite Automata Design and Related Arithmetics. Transactions of the American Mathematical Society, 98(1):21, 1961. URL: https://doi.org/10.2307/1993511.
  22. Joost Engelfriet. Iterated stack automata and complexity classes. Information and Computation, 95(1):21-75, 1991. URL: https://doi.org/10.1016/0890-5401(91)90015-T.
  23. Joost Engelfriet and Vincent van Oostrom. Logical Description of Context-free Graph Languages. Journal of Computer and System Sciences, 55(3):489-503, 1997. URL: https://doi.org/10.1006/jcss.1997.1510.
  24. David Eppstein. Parallel recognition of series-parallel graphs. Information and Computation, 98(1):41-55, 1992. URL: https://doi.org/10.1016/0890-5401(92)90041-D.
  25. Jerome Feder. Plex languages. Information Sciences, 3(3):225-241, 1971. URL: https://doi.org/10.1016/S0020-0255(71)80008-7.
  26. Tomás Feder and Moshe Y. Vardi. Monotone monadic SNP and constraint satisfaction. In 25th annual ACM symposium on Theory of computing (STOC '93), volume Part F1295, pages 612-622. ACM Press, 1993. URL: https://doi.org/10.1145/167088.167245.
  27. Stephen C. Kleene. Representation of Events in Nerve Nets and Finite Automata. In Automata Studies. (AM-34), pages 3-42. Princeton University Press, 1956. Google Scholar
  28. Phokion G. Kolaitis and Moshe Y. Vardi. Conjunctive-Query Containment and Constraint Satisfaction. Journal of Computer and System Sciences, 61(2):302-332, 2000. URL: https://doi.org/10.1006/jcss.2000.1713.
  29. Haas Leiß. Towards Kleene Algebra with recursion. In 5th International Workshop on Computer Science Logic (CSL '91), pages 242-256. Springer, 1991. URL: https://doi.org/10.1007/BFb0023771.
  30. Kamal Lodaya and Pascal Weil. Series-parallel languages and the bounded-width property. Theoretical Computer Science, 237(1-2):347-380, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00031-1.
  31. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9(5):521-530, 1966. URL: https://doi.org/10.1016/S0019-9958(66)80013-X.
  32. Yoshiki Nakamura. Expressive Power and Succinctness of the Positive Calculus of Relations. In 18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS '20), volume 12062 of LNCS, pages 204-220. Springer, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-43520-2_13.
  33. Yoshiki Nakamura. A full version of this paper, 2021. URL: https://yoshikinakamura.bitbucket.io/papers/ep_for_graph.
  34. Mizuhito Ogawa, Zhenjiang Hu, and Isao Sasano. Iterative-free program analysis. In 8th ACM SIGPLAN international conference on Functional programming (ICFP '03), volume 8, pages 111-123. ACM Press, 2003. URL: https://doi.org/10.1145/944705.944716.
  35. Peter W. O'Hearn and David J. Pym. The Logic of Bunched Implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  36. Theodosios Pavlidis. Linear and Context-Free Graph Grammars. Journal of the ACM, 19(1):11-22, 1972. URL: https://doi.org/10.1145/321679.321682.
  37. Andrew M. Pitts. Nominal Sets. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139084673.
  38. David Pym. Resource semantics: logic as a modelling technology. ACM SIGLOG News, 6(2):5-41, 2019. URL: https://doi.org/10.1145/3326938.3326940.
  39. Neil Robertson and Paul D. Seymour. Graph minors. III. Planar tree-width. Journal of Combinatorial Theory, Series B, 36(1):49-64, 1984. URL: https://doi.org/10.1016/0095-8956(84)90013-3.
  40. Benjamin Rossman. Homomorphism preservation theorems. Journal of the ACM, 55(3):1-53, 2008. URL: https://doi.org/10.1145/1379759.1379763.
  41. Alfred Tarski. On the Calculus of Relations. The Journal of Symbolic Logic, 6(3):73-89, 1941. URL: https://doi.org/10.2307/2268577.
  42. Ken Thompson. Programming Techniques: Regular expression search algorithm. Communications of the ACM, 11(6):419-422, 1968. URL: https://doi.org/10.1145/363347.363387.
  43. Boris A. Trakhtenbrot. Finite automata and the logic of monadic predicates (in Russian). Doklady Akademii Nauk SSSR, 140:326-329, 1961. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact