Geodesic
Complexity of Lambek calculi with modalities and of total derivability in grammars
Algebra i logika, Tome 60 (2021) no. 5, pp. 471-496.

Voir la notice de l'article provenant de la source Math-Net.Ru

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 Lambek calculus with modalities — the exponential, under which all structural rules are permitted, and the relevant modality, under which only permutation and contraction rules are allowed. The Lambek calculus with a relevant modality is used in mathematical linguistics. Both calculi are algorithmically undecidable. We consider their fragments in which the modality is allowed to be applied to just formulas of Horn depth not greater than $1$. We prove that these fragments are decidable and belong to the NP class. To show this, in the case of a relevant modality, we introduce a new notion of $\mathcal{R}$-total derivability in context-free grammars, i.e., existence of a derivation in which each rule is used at least a given number of times. It is stated that the $\mathcal{R}$-totality problem is NP-hard for context-free grammars. Also we pinpoint algorithmic complexity of $\mathcal{R}$-total derivability for more general classes of generative grammars.
Mots-clés : Lambek calculus
Keywords: substructural logic, exponential, relevant modality, algorithmic complexity, context-free grammars, total derivability. 
@article{AL_2021_60_5_a1,
     author = {S. M. Dudakov and B. N. Karlov and S. L. Kuznetsov and E. M. Fofanova},
     title = {Complexity of {Lambek} calculi with modalities and of total derivability in grammars},
     journal = {Algebra i logika},
     pages = {471--496},
     publisher = {mathdoc},
     volume = {60},
     number = {5},
     year = {2021},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/AL_2021_60_5_a1/}
}
TY  - JOUR
AU  - S. M. Dudakov
AU  - B. N. Karlov
AU  - S. L. Kuznetsov
AU  - E. M. Fofanova
TI  - Complexity of Lambek calculi with modalities and of total derivability in grammars
JO  - Algebra i logika
PY  - 2021
SP  - 471
EP  - 496
VL  - 60
IS  - 5
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/AL_2021_60_5_a1/
LA  - ru
ID  - AL_2021_60_5_a1
ER  - 
%0 Journal Article
%A S. M. Dudakov
%A B. N. Karlov
%A S. L. Kuznetsov
%A E. M. Fofanova
%T Complexity of Lambek calculi with modalities and of total derivability in grammars
%J Algebra i logika
%D 2021
%P 471-496
%V 60
%N 5
%I mathdoc
%U http://geodesic.mathdoc.fr/item/AL_2021_60_5_a1/
%G ru
%F AL_2021_60_5_a1
S. M. Dudakov; B. N. Karlov; S. L. Kuznetsov; E. M. Fofanova. Complexity of Lambek calculi with modalities and of total derivability in grammars. Algebra i logika, Tome 60 (2021) no. 5, pp. 471-496. http://geodesic.mathdoc.fr/item/AL_2021_60_5_a1/

[1] W. Krull, “Axiomatische Begründung der allgemeinen Idealtheorie”, Sitzber. d. phys.-med. Soc. Erlangen, 56 (1924), 47–63 | Zbl

[2] J. Lambek, “Deductive systems and categories. II: Standard constructions and closed categories”, Category theory, homology theory and their applications I, Proc. conf. (the Seattle Research Center of the Battelle Memorial Institute, June 24–July 19, 1968), Lect. Notes Math., 86, ed. P. Hilton, Springer, Berlin–Heidelberg–New York, 1969, 76–122 | DOI

[3] J.-Y. Girard, “Linear logic”, Theor. Comput. Sci., 50:1 (1987), 1–102 | DOI | Zbl

[4] L. L. Maksimova, “O sisteme aksiom ischisleniya strogoi implikatsii”, Algebra i logika, 3:3 (1964), 59–68 | Zbl

[5] M. Kanovich, S. Kuznetsov, A. Scedrov, “Undecidability of the Lambek calculus with a relevant modality”, Formal grammar, 20th and 21st int. conf., FG 2015 (Barcelona, Spain, August 2015), FG 2016 (Bozen, Italy, August 2016), Lect. Notes Comput. Sci., 9804, eds. A. Foret et al., Springer, Berlin, 2016, 240–256 | DOI | Zbl

[6] M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov, “Subexponentials in non-commutative linear logic”, Math. Struct. Comput. Sci., 29:8 (2019), 1217–1249 | DOI | Zbl

[7] P. Lincoln, J. Mitchell, A. Scedrov, N. Shankar, “Decision problems for propositional linear logic”, Ann. Pure Appl. Logic, 56:1–3 (1992), 239–311 | DOI | Zbl

[8] M. Pentus, “Lambek calculus is NP-complete”, Theor. Comput. Sci., 357:1–3 (2006), 186–201 | DOI | Zbl

[9] Yu. V. Savateev, Algoritmicheskaya slozhnost fragmentov ischisleniya Lambeka, diss. kand. fiz.-mat. nauk, MGU, M., 2009

[10] A. Akho, Dzh. Ulman, Teoriya sintaksicheskogo analiza, perevoda i kompilyatsii, v. 1, Sintaksicheskii analiz, Mir, M., 1978

[11] M. R. Garey, D. S. Johnson, “Complexity results for multiprocessor scheduling under resource constraints”, SIAM J. Comput., 4:4 (1975), 397–411 | DOI | Zbl