Abstract
In his recent papers “Parsing/theorem-proving for logical grammar CatLog3” and “A note on movement in logical grammar”, Glyn Morrill proposes a new substructural calculus to be used as the basis for the categorial grammar parser CatLog3. In this paper we prove that the derivability problem for a fragment of this calculus is algorithmically undecidable.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abrusci, V.M.: A comparison between Lambek syntactic calculus and intuitionistic linear logic. Zeitschr. Math. Logik Grundl. Math. 36, 11–15 (1990). https://doi.org/10.1002/malq.19900360103
Ajdukiewicz, K.: Die syntaktische Konnexität. Stud. Philos. 1, 1–27 (1935)
Bar-Hillel, Y.: A quasi-arithmetical notation for syntactic description. Language 29, 47–58 (1953)
Buszkowski, W.: Some decision problems in the theory of syntactic categories. Zeitschr. Math. Logik Grundl. Math. 28, 539–548 (1982). https://doi.org/10.1002/malq.19820283308
Buszkowski, W., Palka, E.: Infinitary action logic: complexity models and grammars. Stud. Logica. 89(1), 1–18 (2008)
Chomsky, N.: Three models for the description of language. IRE Trans. Inf. Theory I T–2(3), 113–124 (1956)
Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–102 (1987). https://doi.org/10.1016/0304-3975(87)90045-4
Girard, J.-Y.: A new constructive logic: classical logic. Math. Struct. Comput. Sci. 1(3), 255–296 (1991). https://doi.org/10.1017/S0960129500001328
Girard, J.-Y.: On the unity of logic. Ann. Pure Appl. Logic 59(3), 201–217 (1993). https://doi.org/10.1016/0168-0072(93)90093-S
Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998). https://doi.org/10.1006/inco.1998.2700
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, Cham (2016). https://doi.org/10.1007/978-3-319-27683-0_11
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). https://doi.org/10.1007/978-3-662-53042-9_14
Kanovich, M., Kuznetsov, S., Scedrov, A.: Reconciling Lambek’s restriction, cut-elimination, and substitution in the presence of exponential modalities. Annals Pure Applied Logic, accepted for publication. arXiv:1608.02254 (2016)
Kanovich, M., Kuznetsov, S., Scedrov, A.: Undecidability of the Lambek calculus with subexponential and bracket modalities. In: Klasing, R., Zeitoun, M. (eds.) FCT 2017. LNCS, vol. 10472, pp. 326–340. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55751-8_26
Kanovich, M., Kuznetsov, S., Scedrov, A.: Lambek calculus enriched with multiplexing (abstract). In: International Conference of Mal’tsev Meeting 2018, Collection of Abstracts. Sobolev Institute of Mathematics and Novosibirsk State University, Novosibirsk (2018). http://www.math.nsc.ru/conference/malmeet/18/maltsev18.pdf
Kanovich, M., Kuznetsov, S., Nigam, V., Scedrov, A.: Subexponentials in non-commutative linear logic. Math. Struct. Comput. Sci. (2018). https://doi.org/10.1017/S0960129518000117. Accessed 2 May 2018
Kanovich, M., Kuznetsov, S., Nigam, V., Scedrov, A.: A logical framework with commutative and non-commutative subexponentials. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 228–245. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_16
Kozen, D.: On the complexity of reasoning in Kleene algebra. Inf. Comput. 179, 152–162 (2002). https://doi.org/10.1006/inco.2001.2960
Kuznetsov, S.L.: On the Lambek calculus with a unit and one division. Moscow Univ. Math. Bull. 66(4), 173–175 (2011). https://doi.org/10.3103/S0027132211040085
Kuznetsov, S.: The Lambek calculus with iteration: two variants. In: Kennedy, J., de Queiroz, R.J.G.B. (eds.) WoLLIC 2017. LNCS, vol. 10388, pp. 182–198. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55386-2_13
Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci. 318(12), 163–180 (2004). https://doi.org/10.1016/j.tcs.2003.10.018
Lambek, J.: The mathematics of sentence structure. Am. Math. Mon. 65, 154–170 (1958). https://doi.org/10.2307/2310058
Lincoln, P., Mitchell, J., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. Ann. Pure Appl. Logic 56(1–3), 239–311 (1992). https://doi.org/10.1016/0168-0072(92)90075-B
Markov, A.: On the impossibility of certain algorithms in the theory of associative systems. Doklady Acad. Sci. USSR (N. S.) 55, 583–586 (1947)
Moortgat, M.: Multimodal linguistic inference. J. Logic Lang. Inf. 5(3/4), 349–385 (1996). https://doi.org/10.1007/BF00159344
Morrill, G.: Categorial formalisation of relativisation: pied piping, islands, and extraction sites. Technical report LSI-92-23-R, Universitat Politècnica de Catalunya (1992)
Morrill, G.V.: Categorial Grammar: Logical Syntax, Semantics, and Processing. Oxford University Press, Oxford (2011)
Morrill, G., Valentín, O.: Computational coverage of TLG: nonlinearity. In: Proceedings of NLCS 2015. EPiC Series, vol. 32, pp. 51–63 (2015)
Morrill, G.: Grammar logicised: relativisation. Linguist. Philos. 40(2), 119–163 (2017). https://doi.org/10.1007/s10988-016-9197-0
Morrill, G., Kuznetsov, S., Kanovich, M., Scedrov, A.: Bracket induction for Lambek calculus with bracket modalities. In: Foret, A., Kobele, G., Pogodalla, S. (eds.) FG 2018. LNCS, vol. 10950, pp. 84–101. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-662-57784-4_5
Morrill, G.: A note on movement in logical grammar. J. Lang. Model. 6(2), 353–363 (2018). https://doi.org/10.15398/jlm.v6i2.233
Morrill, G.: Parsing/theorem-proving for logical grammar CatLog3. J. Logic Lang. Inf. (2019). https://doi.org/10.1007/s10849-018-09277-w. Accessed 18 Jan 2019
Post, E.L.: Recursive unsolvability of a problem of Thue. J. Symb. Logic 12, 1–11 (1947)
Thue, A.: Probleme über Veränderungen von Zeichenreihen nach gegebener Regeln. Kra. Vidensk. Selsk. Skrifter. 10, 1–34 (1914)
Acknowledgments
Funding
The work of Max Kanovich and Andre Scedrov was supported by the Russian Science Foundation under grant 17-11-01294 and performed at National Research University Higher School of Economics, Moscow, Russia. The work of Stepan Kuznetsov was supported by the Young Russian Mathematics award, by the grant MK-430.2019.1 of the President of Russia, and by the Russian Foundation for Basic Research grant 18-01-00822. Section 3 was contributed by Kanovich and Scedrov. Section 4 was contributed by Kuznetsov. Sections 1, 2, and 5 were contributed jointly and equally by all co-authors.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer-Verlag GmbH Germany, part of Springer Nature
About this paper
Cite this paper
Kanovich, M., Kuznetsov, S., Scedrov, A. (2019). Undecidability of a Newly Proposed Calculus for CatLog3. In: Bernardi, R., Kobele, G., Pogodalla, S. (eds) Formal Grammar. FG 2019. Lecture Notes in Computer Science(), vol 11668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-59648-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-662-59648-7_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-59647-0
Online ISBN: 978-3-662-59648-7
eBook Packages: Computer ScienceComputer Science (R0)