Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Undecidability of the Lambek Calculus with Subexponential and Bracket Modalities

  • Conference paper
  • First Online:
Fundamentals of Computation Theory (FCT 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10472))

Included in the following conference series:

  • 705 Accesses

Abstract

The Lambek calculus is a well-known logical formalism for modelling natural language syntax. The original calculus covered a substantial number of intricate natural language phenomena, but only those restricted to the context-free setting. In order to address more subtle linguistic issues, the Lambek calculus has been extended in various ways. In particular, Morrill and Valentín (2015) introduce an extension with so-called exponential and bracket modalities. Their extension is based on a non-standard contraction rule for the exponential that interacts with the bracket structure in an intricate way. The standard contraction rule is not admissible in this calculus. In this paper we prove undecidability of the derivability problem in their calculus. We also investigate restricted decidable fragments considered by Morrill and Valentín and we show that these fragments belong to the NP class.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Abrusci, V.M.: A comparison between Lambek syntactic calculus and intuitionistic linear propositional logic. Zeitschr. für math. Log. Grundl. Math. (Math. Logic Q.) 36, 11–15 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  2. Ajdukiewicz, K.: Die syntaktische Konnexität. Studia Philos. 1, 1–27 (1935)

    MATH  Google Scholar 

  3. Bar-Hillel, Y.: A quasi-arithmetical notation for syntactic description. Language 29, 47–58 (1953)

    Article  MATH  Google Scholar 

  4. Barry, G., Hepple, M., Leslie, N., Morrill, G.: Proof figures and structural operators for categorial grammar. In: Proceedings of 5th Conference of the European Chapter of ACL, Berlin (1991)

    Google Scholar 

  5. Braüner, T., de Paiva, V.: Cut elimination for full intuitionstic linear logic. BRICS report RS-96-10, April 1996

    Google Scholar 

  6. Braüner, T., de Paiva, V.: A formulation of linear logic based on dependency-relations. In: Nielsen, M., Thomas, W. (eds.) CSL 1997. LNCS, vol. 1414, pp. 129–148. Springer, Heidelberg (1998). doi:10.1007/BFb0028011

    Chapter  Google Scholar 

  7. Braüner, T.: A cut-free Gentzen formulation of modal logic S5. Log. J. IGPL 8(5), 629–643 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  8. Buszkowski, W.: Some decision problems in the theory of syntactic categories. Zeitschr. für math. Logik und Grundl. der Math. (Math. Logic Q.) 28, 539–548 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  9. Buszkowski, W.: Type logics in grammar. In: Hendricks, V.F., Malinowski, J. (eds.) Trends in Logic: 50 Years of Studia Logica, pp. 337–382. Springer, Dordrecht (2003). doi:10.1007/978-94-017-3598-8_12

    Chapter  Google Scholar 

  10. Buszkowski, W.: Lambek calculus with nonlogical axioms. In: Language and Grammar. CSLI Lecture Notes, vol. 168, pp. 77–93 (2005)

    Google Scholar 

  11. Carpenter, B.: Type-Logical Semantics. MIT Press, Cambridge (1997)

    MATH  Google Scholar 

  12. Dekhtyar, M., Dikovsky, A.: Generalized categorial dependency grammars. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 230–255. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78127-1_13

    Chapter  Google Scholar 

  13. Eades III, H., de Paiva, V.: Multiple conclusion linear logic: cut elimination and more. In: Artemov, S., Nerode, A. (eds.) LFCS 2016. LNCS, vol. 9537, pp. 90–105. Springer, Cham (2016). doi:10.1007/978-3-319-27683-0_7

    Chapter  Google Scholar 

  14. Gentzen, G.: Untersuchungen über das logische Schließen I. Math. Z. 39, 176–210 (1935)

    Article  MathSciNet  MATH  Google Scholar 

  15. Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  16. de Groote, P.: On the expressive power of the Lambek calculus extended with a structural modality. In: Language and Grammar. CSLI Lecture Notes, vol. 168, pp. 95–111 (2005)

    Google Scholar 

  17. Kanazawa, M.: Lambek calculus: recognizing power and complexity. In: Gerbrandy, J., et al. (eds.) JFAK. Essays dedicated to Johan van Benthem on the occasion of his 50th birthday. Vossiuspers, Amsterdam University Press, Amsterdam (1999)

    Google Scholar 

  18. Kanovich, M.: The complexity of neutrals in linear logic. In: Proceedings of LICS 1995, pp. 486–495 (1995)

    Google Scholar 

  19. Kanovich, M., Kuznetsov, S., Scedrov, A.: Undecidability of the Lambek calculus with a relevant modality. In: Foret, A., Morrill, G., Muskens, R., Osswald, R., Pogodalla, S. (eds.) FG 2015-2016. LNCS, vol. 9804, pp. 240–256. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53042-9_14. arXiv:1601.06303

    Chapter  Google Scholar 

  20. Kanovich, M., Kuznetsov, S., Scedrov, A.: Undecidability of the Lambek calculus with subexponential and bracket modalities (extended technical report). arXiv:1608.04020 (2017)

  21. Kanovich, M., Kuznetsov, S., Morrill, G., Scedrov, A.: A polynomial time algorithm for the Lambek calculus with brackets of bounded order. arXiv:1705.00694 (2017). Accepted to FSCD 2017

  22. Kuznetsov, S.L.: On the Lambek calculus with a unit and one division. Moscow Univ. Math. Bull. 66(4), 173–175 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  23. Lambek, J.: The mathematics of sentence structure. Amer. Math. Mon. 65(3), 154–170 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  24. Lambek, J.: Deductive systems and categories II. Standard constructions and closed categories. In: Hilton, P.J. (ed.) Category Theory, Homology Theory and their Applications I. LNM, vol. 86, pp. 76–122. Springer, Heidelberg (1969). doi:10.1007/BFb0079385

    Chapter  Google Scholar 

  25. Lincoln, P., Mitchell, J., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. APAL 56, 239–311 (1992)

    MathSciNet  MATH  Google Scholar 

  26. Markov, A.: On the impossibility of certain algorithms in the theory of associative systems. Doklady Acad. Sci. USSR (N.S.) 55, 583–586 (1947)

    MathSciNet  Google Scholar 

  27. Moortgat, M.: Multimodal linguistic inference. J. Log. Lang. Inform. 5(3–4), 349–385 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  28. Moot, R., Retoré, C.: The Logic of Categorial Grammars: A Deductive Account of Natural Language Syntax and Semantics. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31555-8

    Book  MATH  Google Scholar 

  29. Morrill, G.: Categorial formalisation of relativisation: pied piping, islands, and extraction sites. Technical report LSI-92-23-R, Universitat Politècnica de Catalunya (1992)

    Google Scholar 

  30. Morrill, G.V.: Categorial Grammar: Logical Syntax, Semantics, and Processing. Oxford University Press, Oxford (2011)

    Google Scholar 

  31. Morrill, G.: CatLog: a categorial parser/theorem-prover. In: System Demonstration, LACL 2012, Nantes (2012)

    Google Scholar 

  32. Morrill, G.: Grammar logicised: relativisation. Linguist. Philos. 40(2), 119–163 (2017)

    Article  MathSciNet  Google Scholar 

  33. Morrill, G., Valentín, O.: Computational coverage of TLG: nonlinearity. In: Proceedings of NLCS 2015. EPiC Series, vol. 32, pp. 51–63 (2015)

    Google Scholar 

  34. Nigam, V., Miller, D.: Algorithmic specifications in linear logic with subexponentials. In: Proceedings of PPDP 2009, pp. 129–140. ACM (2009)

    Google Scholar 

  35. Pentus, M.: Lambek calculus is NP-complete. Theor. Comput. Sci. 357(1), 186–201 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  36. Pentus, M.: A polynomial time algorithm for Lambek grammars of bounded order. Linguist. Anal. 36(1–4), 441–471 (2010)

    Google Scholar 

  37. Post, E.L.: Recursive unsolvability of a problem of Thue. J. Symb. Log. 12, 1–11 (1947)

    Article  MathSciNet  MATH  Google Scholar 

  38. Ross, J.R.: Constraints on variables in syntax. Ph.D. thesis, MIT (1967)

    Google Scholar 

  39. Steedman, M.: The Syntactic Process. MIT Press, Cambridge, MA (2000)

    MATH  Google Scholar 

  40. Thue, A.: Probleme über Veränderungen von Zeichenreihen nach gegebener Regeln. Kra. Vidensk. Selsk. Skrifter. 10 (1914). (In: Selected Math. Papers, Univ. Forlaget, Oslo, pp. 493–524 (1977))

    Google Scholar 

Download references

Acknowledgements

The work of M. Kanovich and A. Scedrov was supported by the Russian Science Foundation under grant 17-11-01294 and performed at National Research University Higher School of Economics, Russia. The work of S. Kuznetsov was supported by grants RFBR 15-01-09218-a and NŠ-9091.2016.1. Sections 1 and 3 were contributed by S. Kuznetsov, Sects. 2 and 4 by M. Kanovich and A. Scedrov, and Sects. 5, 6, and 7 were contributed jointly and equally by all coauthors.

The authors are grateful to V. de Paiva and T. Braüner for helpful comments on the deep cut elimination procedure.

Author information

Authors and Affiliations

  1. National Research University Higher School of Economics, Moscow, Russian Federation

    Max Kanovich, Stepan Kuznetsov & Andre Scedrov

  2. Steklov Mathematical Institute, RAS, Moscow, Russian Federation

    Stepan Kuznetsov

  3. University of Pennsylvania, Philadelphia, USA

    Andre Scedrov

Authors
  1. Max Kanovich
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stepan Kuznetsov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andre Scedrov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stepan Kuznetsov .

Editor information

Editors and Affiliations

  1. CNRS, University of Bordeaux, Talence cedex, France

    Ralf Klasing

  2. LaBRI, University of Bordeaux, Talence cedex, France

    Marc Zeitoun

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer-Verlag GmbH Germany

About this paper

Cite this paper

Kanovich, M., Kuznetsov, S., Scedrov, A. (2017). Undecidability of the Lambek Calculus with Subexponential and Bracket Modalities. In: Klasing, R., Zeitoun, M. (eds) Fundamentals of Computation Theory. FCT 2017. Lecture Notes in Computer Science(), vol 10472. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55751-8_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-55751-8_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-55750-1

  • Online ISBN: 978-3-662-55751-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation