• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • Undecidability of the Lambek Calculus with Subexponential and Bracket Modalities
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
May 14, 2026
Resource Race and Green Transition: Three Unexpected Conclusions from Foresight Centres Research on Climate and Poverty
Beneath the surface of green energy—which most people associate with solar panels, electric vehicles, and reduced CO2 emissions—lies a complex web of geopolitical interests, international inequality, and resource constraints. Researchers from the Laboratory for Science and Technology Studies (LST) at the HSE ISSEK Foresight Centre have published a series of articles in leading international journals on hidden and overt conflicts surrounding critically important metals and minerals, as well as related processes in the energy sector.
May 13, 2026
Immersion in Second Language Environment Influences Bilinguals Perception of Emotions
Researchers at the Cognitive Health and Intelligence Centre at the HSE Institute for Cognitive Neuroscience have discovered how bilingual individuals process emotional words in their native (first) and non-native (second) languages. It was found that the link between word meaning and bodily sensations is weaker in a second language than in a first language. However, the more a person is immersed in a language environment, the smaller this difference becomes. The article has been published in Language, Cognition and Neuroscience.
May 12, 2026
‘Any Real-Economy Company Can Use Our Products
The HSE Centre for Financial Research and Data Analytics combines fundamental and applied work, including in areas unique to Russia such as the connection between sentiment in the media and social networks and financial markets. The HSE News Service spoke with the centre’s director, Professor Tamara Teplova, about its work.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

Undecidability of the Lambek Calculus with Subexponential and Bracket Modalities

P. 326–340.
Kanovich M., Scedrov A., Kuznetsov S.

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.

Language: English
DOI
Text on another site
Keywords: Lambek calculus
Publication based on the results of:
Explanation-oriented Methods of  Data Analysis for Semantically Rich Data and Their Applications (2017)

In book

21st International Symposium, Fundamentals of Computation Theory 2017, FCT 2017
Springer, 2017.
Similar publications
On syntactic concept lattice models for the Lambek calculus and infinitary action logic
Stepan L. Kuznetsov, Journal of Logic and Computation 2026 Vol. 36 No. 1 Article exaf078
The linguistic applications of the Lambek calculus suggest its semantics over algebras of formal languages. A straightforward approach to construct such semantics indeed yields a brilliant completeness theorem (Pentus 1995, Ann. Pure Appl. Logic, 75, 179–213). However, extending the calculus with extra operations ruins completeness. In order to mitigate this issue, Wurm (2017, J. Logic Lang. Inf., ...
Added: January 14, 2026
Infinitary action logic with exponentiation
Kuznetsov S., Speranski S. O., Annals of Pure and Applied Logic 2022 Vol. 173 No. 2 Article 103057
We introduce infinitary action logic with exponentiation — that is, the multiplicative-additive Lambek calculus extended with Kleene star and with a family of subexponential modalities, which allow some of the structural rules (contraction, weakening, permutation). The logic is presented in the form of an infinitary sequent calculus. We prove cut elimination and, in the case ...
Added: December 26, 2025
Infinitary action logic with multiplexing
Kuznetsov S., Speranski S. O., Studia Logica 2023 Vol. 111 No. 2 P. 251–280
Infinitary action logic can be naturally expanded by adding exponential and subexponential modalities from linear logic. In this article we shall develop infinitary action logic with a subexponential that allows multiplexing (instead of contraction). Both non-commutative and commutative versions of this logic will be considered, presented as infinitary sequent calculi. We shall prove cut admissibility ...
Added: December 26, 2025
Craig's trick and a non-sequential system for the Lambek calculus and its fragments
Kuznetsov S., Lugovaya V., Ryzhova A., Logic Journal of the IGPL 2019 Vol. 27 No. 3 P. 252–266
Added: May 1, 2025
Syntactic concept lattice models for infinitary action logic
Stepan L. Kuznetsov, , in: Logic, Language, Information, and Computation: 30th International Workshop, WoLLIC 2024, Bern, Switzerland, June 10–13, 2024, ProceedingsVol. 14672: Lecture Notes in Computer Science.: Cham: Springer, 2024. P. 93–107.
Added: June 12, 2024
Making first order linear logic a generating grammar
Sergey Slavnov, Logical Methods in Computer Science 2023 Vol. 19 No. 4
It is known that different categorial grammars have surface representation in a fragment of first order multiplicative linear logic (MLL1). We show that the fragment of interest is equivalent to the recently introduced extended tensor type calculus (ETTC). ETTC is a calculus of specific typed terms, which represent tuples of strings, more precisely bipartite graphs ...
Added: December 20, 2023
COMPLEXITY OF LAMBEK CALCULI WITH MODALITIES AND OF TOTAL DERIVABILITY IN GRAMMARS
S. M. Dudakov, Karlov B. N., S. L. Kuznetsov et al., Algebra and Logic 2021 Vol. 60 No. 5 P. 308–326
The Lambek calculus with the unit can be defined as the atomic theory (algebraic logic) of the class of residuated monoids. This calculus, being a theory of a broader class of algebras than Heyting ones, is weaker than intuitionistic logic. Namely, it lacks structural rules: permutation, contraction, and weakening. We consider two extensions of the ...
Added: November 12, 2023
Decidable Fragments of Calculi Used in CatLog
Kanovich M., Kuznetsov Stepan G., Kuznetsov S. et al., Studies in Computational Intelligence 2021 Vol. 999 P. 1–24
CatLog is a categorial grammar parser/theorem-prover developed by Glyn Morrill and his co-authors. CatLog is based on an extension of Lambek calculus. A distinctive feature of this extension is the usage of brackets for controlled non-associativity and a subexponential modality whose contraction rule interacts with bracketing in a sophisticated way. We consider two variants of the calculus, appearing in different versions ...
Added: December 14, 2021
Language models for some extensions of the Lambek calculus
Kanovich M., Kuznetsov S., Scedrov A., Information and Computation 2022 Vol. 287 Article 104760
We investigate language interpretations of two extensions of the Lambek calculus: with additive conjunction and disjunction and with additive conjunction and the unit constant. For extensions with additive connectives, we show that conjunction and disjunction behave differently. Adding both of them leads to incompleteness due to the distributivity law. We show that with conjunction only ...
Added: December 4, 2021
On embedding Lambek calculus into commutative categorial grammars
Slavnov S. A., Journal of Logic and Computation 2022 Vol. 32 No. 3 P. 479–517
We consider tensor grammars, which are an example of ‘commutative’ grammars, based on the classical (rather than intuitionistic) linear logic. They can be seen as a surface representation of abstract categorial grammars (ACG) in the sense that derivations of ACG translate to derivations of tensor grammars and this translation is isomorphic on the level of string ...
Added: October 21, 2021
The multiplicative-additive Lambek calculus with subexponential and bracket modalities
Kanovich M., Kuznetsov S., Scedrov A., Journal of Logic, Language and Information 2021 Vol. 30 No. 1 P. 31–88
We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill’s calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the ! subexponential modality. For ...
Added: November 25, 2020
A \(\Pi^0_1\)-bounded fragment of infinitary action logic with exponential
Kuznetsov S., , in: Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th BirthdayIssue 12300.: Cham: Springer, 2020. P. 3–16.
Infinitary action logic is an extension of the multiplicative-additive Lambek calculus with Kleene iteration, axiomatized by an 𝜔-rule. Buszkowski and Palka (2007) show that this logic is \(\Pi^0_1\)-complete. As shown recently by Kuznetsov and Speranski, the extension of infinitary action logic with the exponential modality is much harder: \(\Pi^1_1\)-complete. The raise of complexity is of ...
Added: November 25, 2020
Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities
Kanovich M., Kuznetsov S., Scedrov A., Journal of Logic and Computation 2020 Vol. 30 No. 1 P. 239–256
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality ...
Added: July 1, 2020
The complexity of multiplicative-additive Lambek calculus: 25 years later
Kanovich M., Kuznetsov S., Scedrov A., , in: Logic, Language, Information, and Computation: 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, ProceedingsVol. 11541: Lecture Notes in Computer Science.: Berlin, Heidelberg: Springer, 2019. P. 356–372.
The Lambek calculus was introduced as a mathematical description of natural languages. The original Lambek calculus is NP-complete (Pentus), while its product-free fragment with only one implication is polynomially decidable (Savateev). We consider Lambek calculus with the additional connectives: conjunction and disjunction. It is known that this system is PSPACE-complete (Kanovich, Kanazawa). We prove, in ...
Added: September 4, 2019
L-models and R-models for Lambek calculus enriched with additives and the multiplicative unit
Kanovich M., Kuznetsov S., Scedrov A., , in: Logic, Language, Information, and Computation: 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, ProceedingsVol. 11541: Lecture Notes in Computer Science.: Berlin, Heidelberg: Springer, 2019. P. 373–391.
Language and relational models, or L-models and R-models, are two natural classes of models for the Lambek calculus. Completeness w.r.t. L-models was proved by Pentus and completeness w.r.t. R-models by Andréka and Mikulás. It is well known that adding both additive conjunction and disjunction together yields incompleteness, because of the distributive law. The product-free Lambek ...
Added: September 4, 2019
A Logical Framework with Commutative and Non-commutative Subexponentials
Kanovich M., Kuznetsov S., Nigam V. et al., , in: 9TH INTERNATIONAL JOINT CONFERENCE ON AUTOMATED REASONINGIssue 10900.: Springer International Publishing AG, part of Springer Nature 2018, 2018. P. 228–245.
Logical frameworks allow the specification of deductive systems using the same logical machinery. Linear logical frameworks have been successfully used for the specification of a number of computational, logics and proof systems. Its success relies on the fact that formulas can be distinguished as linear, which behave intuitively as resources, and unbounded, which behave intuitionistically. ...
Added: July 11, 2018
A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order
Kanovich M., Kuznetsov S., Morrill G. et al., , in: Second International Conference on Formal Structures for Computation and Deduction, FSCD 2017Vol. 84: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017).: [б.и.], 2017. P. 22:1–22:17.
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 ...
Added: September 15, 2017
Trivalent logics arising from L-models for the Lambek calculus with constants
S. L. Kuznetsov, Journal of Applied Non-Classical Logics 2014 Vol. 14 No. 1-2 P. 132–137
We consider language models for the Lambek calculus that allow empty antecedents and enrich them with constants for the empty language and for the language containing only the empty word. No complete calculi are known with respect to these semantics, and in this paper we consider several trivalent systems that arise as fragments of these ...
Added: October 23, 2016
On Lambek’s Restriction in the Presence of Exponential Modalities
Kanovich M., Kuznetsov S., Scedrov A., , in: Symposium on Logical Foundations of Computer Science (LFCS 2016)Vol. 9537: Logical Foundations of Computer Science.: Springer, 2016. P. 146–158.
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called “Lambek’s restriction,” that is, the antecedent of any provable sequent should be non-empty. In this paper we discuss ways of extending the Lambek calculus with the linear logic exponential ...
Added: June 28, 2016
Product-Free Lambek Calculus Is NP-Complete
Savateev Y., Annals of Pure and Applied Logic 2012 Vol. 163 P. 775–788
In this paper we prove that the derivability problems for product-free Lambek calculus and product-free Lambek calculus allowing empty premises are NP-complete. Also we introduce a new derivability characterization for these calculi. ...
Added: October 20, 2014
Применение сетей доказательств для исследования фрагментов исчисления Ламбека
Savateev Y., Известия РАН. Серия математическая 2011 Т. 75 № 3 С. 189–222
We use proof-nets to study the algorithmic complexity of the derivability problem for some fragments of the Lambek calculus. We prove the NP-completeness of this problem for the unidirectional fragment and the product-free fragment, and also for versions of these fragments that admit empty antecedents. ...
Added: October 20, 2014
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit