Document Open Access Logo

First-Order Intuitionistic Linear Logic and Hypergraph Languages

Author Tikhon Pshenitsyn

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2025.170.pdf
  • Filesize: 1.42 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Grammars and context-free languages
  • Theory of computation → Rewrite systems
Keywords
  • linear logic
  • categorial grammar
  • MILL1 grammar
  • first-order logic
  • hypergraph language
  • graph transformation
  • language semantics
  • HR-algebra

Metrics

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

Abstract

The Lambek calculus is a substructural logic known to be closely related to the formal language theory: on the one hand, it is used for generating formal languages by means of categorial grammars and, on the other hand, it has formal language semantics, with respect to which it is sound and complete. This paper studies a similar relation between first-order intuitionistic linear logic ILL1 along with its multiplicative fragment MILL1 on the one hand and the hypergraph grammar theory on the other. In the first part, we introduce a novel concept of hypergraph first-order logic categorial grammar, which is a generalisation of string MILL1 grammars introduced in Richard Moot’s works. We prove that hypergraph ILL1 grammars generate all recursively enumerable hypergraph languages and that hypergraph MILL1 grammars are as powerful as linear-time hypergraph transformation systems. In addition, we show that the class of languages generated by string MILL1 grammars is closed under intersection and that it includes a non-semilinear language as well as an NP-complete one. This shows how much more powerful string MILL1 grammars are as compared to Lambek categorial grammars. In the second part, we develop hypergraph language models for MILL1. In such models, formulae of the logic are interpreted as hypergraph languages and multiplicative conjunction is interpreted using parallel composition, which is one of the operations of HR-algebras introduced by Courcelle. We prove completeness of the universal-implicative fragment of MILL1 with respect to these models and thus present a new kind of semantics for a fragment of first-order linear logic.

Cite As Get BibTex

Tikhon Pshenitsyn. First-Order Intuitionistic Linear Logic and Hypergraph Languages. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 170:1-170:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ICALP.2025.170

Author Details

Tikhon Pshenitsyn
  • Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russian Federation

Funding

This work was supported by the Russian Science Foundation under grant no. 23-11-00104, https://rscf.ru/en/project/23-11-00104/.

Acknowledgements

I thank Richard Moot and Sergei Slavnov for their attention to my work and for the productive discussions. I am also grateful to the anonymous reviewers for valuable remarks.

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. URL: https://doi.org/10.1093/logcom/2.3.297.
  2. Ronald V. Book. Time-bounded grammars and their languages. Journal of Computer and System Sciences, 5(4):397-429, 1971. URL: https://doi.org/10.1016/S0022-0000(71)80025-9.
  3. Ronald V. Book. On the complexity of formal grammars. Acta Informatica, 9:171-181, 1978. URL: https://doi.org/10.1007/BF00289076.
  4. Wojciech Buszkowski. Compatibility of a categorial grammar with an associated category system. Mathematical Logic Quarterly, 28(14-18):229-238, 1982. URL: https://doi.org/10.1002/malq.19820281407.
  5. Wojciech Buszkowski. Type Logics in Grammar, pages 337-382. Springer Netherlands, Dordrecht, 2003. URL: https://doi.org/10.1007/978-94-017-3598-8_12.
  6. Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation, 85(1):12-75, 1990. URL: https://doi.org/10.1016/0890-5401(90)90043-H.
  7. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012. Google Scholar
  8. Frank Drewes, Hans-Jörg Kreowski, and Annegret Habel. Hyperedge replacement graph grammars. In Grzegorz Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pages 95-162. World Scientific, 1997. URL: https://doi.org/10.1142/9789812384720_0002.
  9. Joost Engelfriet. Context-free graph grammars. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 125-213. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_3.
  10. Jean-Yves Girard. Linear logic: A survey. In Friedrich L. Bauer, Wilfried Brauer, and Helmut Schwichtenberg, editors, Logic and Algebra of Specification, pages 63-112, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-58041-3_3.
  11. Aleksei Gladkii. On complexity of inference in phase-structure grammars. Algebra i Logika. Sem. (in Russian), 3(5-6):29-44, 1964. Google Scholar
  12. Annegret Habel. Hyperedge Replacement: Grammars and Languages, volume 643 of Lecture Notes in Computer Science. Springer, 1992. URL: https://doi.org/10.1007/BFB0013875.
  13. Annegret Habel, Jürgen Müller, and Detlef Plump. Double-pushout graph transformation revisited. Mathematical Structures in Computer Science, 11(5):637-688, 2001. URL: https://doi.org/10.1017/S0960129501003425.
  14. Laura Kallmeyer. Parsing Beyond Context-Free Grammars. Springer Berlin Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-14846-0.
  15. Max I. Kanovich, Mitsuhiro Okada, and Kazushige Terui. Intuitionistic phase semantics is almost classical. Mathematical. Structures in Comp. Sci., 16(1):67-86, 2006. URL: https://doi.org/10.1017/S0960129505005062.
  16. Yuichi Komori. Predicate logics without the structure rules. Studia Logica, 45(4):393-404, 1986. URL: https://doi.org/10.1007/bf00370272.
  17. Barbara König, Dennis Nolte, Julia Padberg, and Arend Rensink. A tutorial on graph transformation. In Reiko Heckel and Gabriele Taentzer, editors, Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig, volume 10800 of Lecture Notes in Computer Science, pages 83-104. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75396-6_5.
  18. Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154-170, 1958. URL: https://doi.org/10.1080/00029890.1958.11989160.
  19. Michael Moortgat. Multimodal linguistic inference. Journal of Logic, Language and Information, 5(3–4):349-385, 1996. URL: https://doi.org/10.1007/bf00159344.
  20. Richard Moot. Extended Lambek calculi and first-order linear logic. In Claudia Casadio, Bob Coecke, Michael Moortgat, and Philip J. Scott, editors, Categories and Types in Logic, Language, and Physics - Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, volume 8222 of Lecture Notes in Computer Science, pages 297-330. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54789-8_17.
  21. Richard Moot. Hybrid type-logical grammars, first-order linear logic and the descriptive inadequacy of lambda grammars, 2014. URL: https://arxiv.org/abs/1405.6678.
  22. Richard Moot and Mario Piazza. Linguistic applications of first order intuitionistic linear logic. Journal of Logic, Language and Information, 10(2):211-232, 2001. URL: https://doi.org/10.1023/a:1008399708659.
  23. Richard Moot and Christian Retoré. The Logic of Categorial Grammars - A Deductive Account of Natural Language Syntax and Semantics, volume 6850 of Lecture Notes in Computer Science. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31555-8.
  24. Glyn Morrill, Oriol Valentín, and Mario Fadda. The displacement calculus. Journal of Logic, Language and Information, 20(1):1-48, 2010. URL: https://doi.org/10.1007/s10849-010-9129-2.
  25. Mati Pentus. Lambek grammars are context free. In Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pages 429-433, 1993. URL: https://doi.org/10.1109/LICS.1993.287565.
  26. Mati Pentus. Models for the Lambek calculus. Ann. Pure Appl. Log., 75(1-2):179-213, 1995. URL: https://doi.org/10.1016/0168-0072(94)00063-9.
  27. Mati Pentus. Lambek calculus is NP-complete. Theoretical Computer Science, 357(1):186-201, 2006. Clifford Lectures and the Mathematical Foundations of Programming Semantics. URL: https://doi.org/10.1016/j.tcs.2006.03.018.
  28. Tikhon Pshenitsyn. Hypergraph Lambek grammars. Journal of Logical and Algebraic Methods in Programming, 129:100798, 2022. URL: https://doi.org/10.1016/j.jlamp.2022.100798.
  29. Tikhon Pshenitsyn. Commutative Lambek grammars. Journal of Logic, Language and Information, 32(5):887-936, 2023. URL: https://doi.org/10.1007/s10849-023-09407-z.
  30. Tikhon Pshenitsyn. First-order intuitionistic linear logic and hypergraph languages, 2025. URL: https://doi.org/10.48550/arXiv.2502.05816.
  31. Grzegorz Rozenberg. Handbook of Graph Grammars and Computing by Graph Transformation. World Scientific, 1997. URL: https://doi.org/10.1142/3303.
  32. Sylvain Salvati. A note on the complexity of abstract categorial grammars. In Christian Ebert, Gerhard Jäger, and Jens Michaelis, editors, The Mathematics of Language, pages 266-271, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  33. Harold Shellinx. Some syntactical observations on linear logic. Journal of Logic and Computation, 1(4):537-559, September 1991. URL: https://doi.org/10.1093/logcom/1.4.537.
  34. Sergey Slavnov. Making first order linear logic a generating grammar. Logical Methods in Computer Science, Volume 19, Issue 4, 2023. URL: https://doi.org/10.46298/lmcs-19(4:11)2023.
  35. Kohtaro Tadaki, Tomoyuki Yamakami, and Jack C.H. Lin. Theory of one-tape linear-time Turing machines. Theoretical Computer Science, 411(1):22-43, 2010. URL: https://doi.org/10.1016/j.tcs.2009.08.031.
  36. Tadahiro Uesu. A system of graph grammars which generates all recursively enumerable sets of labelled graphs. Tsukuba Journal of Mathematics, 2(none):11-26, 1978. URL: https://doi.org/10.21099/tkbjm/1496158502.
  37. Johan van Benthem. Language in Action: Categories, Lambdas and Dynamic Logic. MIT Press, 1995. 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