Document Open Access Logo

A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2017.22.pdf
  • Filesize: 0.57 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • Lambek calculus
  • proof nets
  • Lambek calculus with brackets
  • categorial grammar
  • polynomial algorithm

Metrics

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

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSCD.2017.22

Author Details

Max Kanovich
Stepan Kuznetsov
Glyn Morrill
Andre Scedrov

References

  1. E. Aarts. Proving theorems of second order Lambek calculus in polynomial time. Studia Logica, 53:373-387, 1994. Google Scholar
  2. E. Aarts and K. Trautwein. Non-associative Lambek categorial grammar in polynomial time. Math. Logic Quart., 41:476-484, 1995. Google Scholar
  3. V. M. Abrusci. Non-commutative proof nets. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic. Cambridge University Press, 1995. Google Scholar
  4. K. Ajdukiewicz. Die syntaktische Konnexität. Studia Philosophica, 1:1-27, 1935. Google Scholar
  5. Y. Bar-Hillel. A quasi-arithmetical notation for syntactic description. Language, 29:47-58, 1953. Google Scholar
  6. W. Buszkowski. Type logics in grammar. In Trends in Logic: 50 Years of Studia Logica, pages 337-382. Springer, 2003. Google Scholar
  7. B. Carpenter. Type-Logical Semantics. MIT Press, Cambridge, MA, 1997. Google Scholar
  8. V. Danos and L. Regnier. The structure of multiplicatives. Arch. Math. Log., 28:181-203, 1989. Google Scholar
  9. Ph. de Groote. A dynamic programming approach to categorial deduction. In H. Ganzinger, editor, Proc. CADE 1999, volume 1632 of Lect. Notes Comput. Sci., pages 1-15. Springer, 1999. Google Scholar
  10. Ph. de Groote. The non-associative Lambek calculus with product in polynomial time. In Proc. TABLEAUX 1999, pages 128-139. Springer, 1999. Google Scholar
  11. M. Fadda and G. Morrill. The Lambek calculus with brackets. In Language and Grammar: Studies in Mathematical Linguistics and Natural Language, pages 113-128. CSLI, Jan 2005. Google Scholar
  12. T. Fowler. Efficient parsing with the product-free Lambek calculus. In Proc. COLING 2008, 2008. Google Scholar
  13. T. Fowler. A polynomial time algorithm for parsing with the bounded order Lambek calculus. In Proc. MoL 2009, 2009. Google Scholar
  14. S. Ginsburg. The mathematical theory of context-free languages. McGraw-Hill, 1966. Google Scholar
  15. J.-Y. Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  16. G. Jäger. On the generative capacity of multi-modal categorial grammars. Research on Language and Computation, 1(1-2):105-125, 2003. Google Scholar
  17. G. Jäger. Anaphora and Type Logical Grammar, volume 24 of Trends in Logic - Studia Logica Library. Springer, Dordrecht, 2005. Google Scholar
  18. M. Kanovich, S. Kuznetsov, and A. Scedrov. Undecidability of the Lambek calculus with a relevant modality. In Proc. Formal Grammar 2015 and 2016, volume 9804 of Lect. Notes Comput. Sci., pages 240-256. Springer, 2016. Google Scholar
  19. N. Kurtonina. Frames and labels. A modal analysis of categorial inference. PhD thesis, Universiteit Utrecht, ILLC, Amsterdam, 1995. Google Scholar
  20. S. Kuznetsov. Lambek grammars with one division and one primitive type. Log. J. IGPL, 20(1):207-221, 2012. Google Scholar
  21. S. L. Kuznetsov. On translating Lambek grammars with one division into context-free grammars. Proc. Steklov Inst. Math., 294:129-138, 2016. Google Scholar
  22. F. Lamarche and C. Retoré. Proof nets for the Lambek calculus - an overview. In V. M. Abrusci and C. Casadio, editors, Proofs and Linguistic Categories, Proc. 1996 Roma Workshop, pages 241-262. CLUEB, 1996. Google Scholar
  23. J. Lambek. The mathematics of sentence structure. Amer. Math. Mon., 65:154-170, 1958. Google Scholar
  24. J. Lambek. On the calculus of syntactic types. In Structure of Language and Its Mathematical Aspects, volume 12 of Proc. Symposia Appl. Math., pages 166-178. AMS, 1961. Google Scholar
  25. M. Moortgat. Multimodal linguistic inference. J. Log. Lang. Inform., 5(3, 4):349-385, 1996. Google Scholar
  26. R. Moot and C. Retoré. The Logic of Categorial Grammars: A Deductive Account of Natural Language Syntax and Semantics. Springer, Heidelberg, 2012. Google Scholar
  27. G. Morrill. Categorial formalisation of relativisation: pied piping, islands, and extraction sites. Technical Report LSI-92-23-R, Universitat Politècnica de Catalunya, 1992. Google Scholar
  28. G. V. Morrill. Categorial Grammar: Logical Syntax, Semantics, and Processing. Oxford University Press, 2011. Google Scholar
  29. M. Nagayama and M. Okada. A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic. Theor. Comput. Sci., 294:551-573, 2003. Google Scholar
  30. G. Penn. A graph-theoretic approach to sequent derivability in the Lambek calculus. Electr. Notes Theor. Comput. Sci., 53, 2002. Google Scholar
  31. M. Pentus. Lambek grammars are context-free. In Proc. LICS 1993, pages 430-433, Montreal, 1993. Google Scholar
  32. M. Pentus. Models for the Lambek calculus. Ann. Pure Appl. Log., 75(1-2):179-213, 1995. Google Scholar
  33. M. Pentus. Free monoid completeness of the Lambek calculus allowing empty premises, volume 12 of Lecture Notes in Logic, pages 171-209. Springer-Verlag, Berlin, 1998. Google Scholar
  34. M. Pentus. Lambek calculus is NP-complete. Theor. Comput. Sci., 357(1):186-201, 2006. Google Scholar
  35. M. Pentus. A polynomial-time algorithm for Lambek grammars of bounded order. Linguistic Analysis, 36(1-4):441-471, 2010. Google Scholar
  36. Yu. Savateev. Unidirectional Lambek grammars in polynomial time. Theory Comput. Syst., 46(4):662-672, 2010. Google Scholar
  37. K. Versmissen. Grammatical composition: modes, models, modalities. PhD thesis, OTS Utrecht, 1996. Google Scholar
  38. D. N. Yetter. Quantales and (noncommutative) linear logic. J. Symb. Log., 55(1):41-64, 1990. 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