2 Search Results for "Morrill, Glyn"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.170
First-Order Intuitionistic Linear Logic and Hypergraph Languages

Authors: Tikhon Pshenitsyn

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{pshenitsyn:LIPIcs.ICALP.2025.170,
  author =	{Pshenitsyn, Tikhon},
  title =	{{First-Order Intuitionistic Linear Logic and Hypergraph Languages}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{170:1--170:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.170},
  URN =		{urn:nbn:de:0030-drops-235473},
  doi =		{10.4230/LIPIcs.ICALP.2025.170},
  annote =	{Keywords: linear logic, categorial grammar, MILL1 grammar, first-order logic, hypergraph language, graph transformation, language semantics, HR-algebra}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.22
A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order

Authors: Max Kanovich, Stepan Kuznetsov, Glyn Morrill, and Andre Scedrov

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. Pentus (2010) gave a polynomial-time algorithm for determining provability of bounded depth formulas in L*, the Lambek calculus with empty antecedents allowed. Pentus' algorithm is based on tabularisation of proof nets. Lambek calculus with brackets is a conservative extension of Lambek calculus with bracket modalities, suitable for the modeling of syntactical domains. In this paper we give an algorithm for provability in Lb*, the Lambek calculus with brackets allowing empty antecedents. Our algorithm runs in polynomial time when both the formula depth and the bracket nesting depth are bounded. It combines a Pentus-style tabularisation of proof nets with an automata-theoretic treatment of bracketing.
Cite as

Max Kanovich, Stepan Kuznetsov, Glyn Morrill, and Andre Scedrov. A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kanovich_et_al:LIPIcs.FSCD.2017.22,
  author =	{Kanovich, Max and Kuznetsov, Stepan and Morrill, Glyn and Scedrov, Andre},
  title =	{{A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.22},
  URN =		{urn:nbn:de:0030-drops-77387},
  doi =		{10.4230/LIPIcs.FSCD.2017.22},
  annote =	{Keywords: Lambek calculus, proof nets, Lambek calculus with brackets, categorial grammar, polynomial algorithm}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2017

  • Refine by Author
  • 1 Kanovich, Max
  • 1 Kuznetsov, Stepan
  • 1 Morrill, Glyn
  • 1 Pshenitsyn, Tikhon
  • 1 Scedrov, Andre

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Grammars and context-free languages
  • 1 Theory of computation → Linear logic
  • 1 Theory of computation → Rewrite systems

  • Refine by Keyword
  • 2 categorial grammar
  • 1 HR-algebra
  • 1 Lambek calculus
  • 1 Lambek calculus with brackets
  • 1 MILL1 grammar
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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