Undecidability of the Lambek calculus with a relevant modality. (English) Zbl 1478.03043
Foret, Annie (ed.) et al., Formal grammar. 20th and 21st international conferences, FG 2015, Barcelona, Spain, August 2015. Revised selected papers. FG 2016, Bozen, Italy, August 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9804, 240-256 (2016).
Summary: Morrill and Valentín in the paper “Computational coverage of TLG: nonlinearity” [12] considered an extension of the Lambek calculus enriched by a so-called “exponential” modality. This modality behaves in the “relevant” style, that is, it allows contraction and permutation, but not weakening. Morrill and Valentín stated an open problem whether this system is decidable. Here we show its undecidability. Our result remains valid if we consider the fragment where all division operations have one direction. We also show that the derivability problem in a restricted case, where the modality can be applied only to variables (primitive types), is decidable and belongs to the NP class.
For the entire collection see [Zbl 1343.68007].
For the entire collection see [Zbl 1343.68007].
MSC:
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 03B25 | Decidability of theories and sets of sentences |
| 03F52 | Proof-theoretic aspects of linear logic and other substructural logics |
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Abrusci, V.M.: A comparison between Lambek syntactic calculus and intuitionistic linear propositional logic. Zeitschr. für math. Logik und Grundl. der Math. (Math. Logic Q.) 36, 11–15 (1990) · Zbl 0719.03005 · doi:10.1002/malq.19900360103 |
| [2] | 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) · Zbl 0499.03010 · doi:10.1002/malq.19820283308 |
| [3] | Buszkowski, W.: Lambek calculus with nonlogical axioms. In: Language and Grammar. CSLI Lecture Notes, vol. 168, pp. 77–93 (2005) |
| [4] | Carpenter, B.: Type-Logical Semantics. MIT Press, Cambridge (1998) · Zbl 0913.68133 |
| [5] | Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1–102 (1987) · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4 |
| [6] | Kanazawa, M., Salvati, S.: The string-meaning relations definable by Lambek grammars and context-free grammars. In: Morrill, G., Nederhof, M.-J. (eds.) Formal Grammar 2012 and 2013. LNCS, vol. 8036, pp. 191–208. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39998-5_12 · Zbl 1390.68366 · doi:10.1007/978-3-642-39998-5_12 |
| [7] | Kanovich, M., Kuznetsov, S., Scedrov, A.: On Lambek’s restriction in the presence of exponential modalities. In: Artemov, S., Nerode, A. (eds.) LFCS 2016. LNCS, vol. 9537, pp. 146–158. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-27683-0_11 · Zbl 1476.03026 · doi:10.1007/978-3-319-27683-0_11 |
| [8] | Kuznetsov, S.L.: On translating context-free grammars into Lambek grammars. Proc. Steklov Inst. Math. 290, 63–69 (2015) · Zbl 1333.68171 · doi:10.1134/S0081543815060061 |
| [9] | Lambek, J.: The mathematics of sentence structure. Am. Math. Mon. 65(3), 154–170 (1958) · Zbl 0080.00702 · doi:10.2307/2310058 |
| [10] | Lambek, J.: On the calculus of syntactic types. In: Proceedings of Symposia in Applied Mathematics: Structure of Language and its Mathematical Aspects, vol. 12, pp. 166–178. AMS (1961) · doi:10.1090/psapm/012/9972 |
| [11] | Lincoln, P., Mitchell, J., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. Ann. Pure Appl. Logic 56(1–3), 239–311 (1992) · Zbl 0768.03003 · doi:10.1016/0168-0072(92)90075-B |
| [12] | Morrill, G., Valentín, O.: Computational coverage of TLG: nonlinearity. In: Proceedings of NLCS 2015. EPiC Series, vol. 32, pp. 51–63 (2015) |
| [13] | Pentus, M.: Product-free Lambek calculus and context-free grammars. J. Symbolic Logic 62(2), 648–660 (1997) · Zbl 0882.68084 · doi:10.2307/2275553 |
| [14] | Pentus, M.: Lambek calculus is NP-complete. Theor. Comput. Sci. 357, 186–201 (2006) · Zbl 1104.03013 · doi:10.1016/j.tcs.2006.03.018 |
| [15] | Pentus, M.: Complexity of the Lambek calculus and its fragments. Adv. Modal Logic 8, 310–329 (2010). College Publications · Zbl 1254.03044 |
| [16] | Savateev, Y.: Lambek grammars with one division are decidable in polynomial time. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) Computer Science – Theory and Applications. LNCS, vol. 5010, pp. 273–282. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-79709-8_28 · Zbl 1142.68415 · doi:10.1007/978-3-540-79709-8_28 |
| [17] | Savateev, Y.: Product-free Lambek calculus is NP-complete. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 380–394. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-92687-0_26 · Zbl 1211.03041 · doi:10.1007/978-3-540-92687-0_26 |
| [18] | Yetter, D.N.: Quantales and (noncommutative) linear logic. J. Symbolic Logic 55(1), 41–64 (1990) · Zbl 0701.03026 · doi:10.2307/2274953 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
