Logical foundations for hybrid type-logical grammars. (English) Zbl 1515.03115
Summary: This paper explores proof-theoretic aspects of hybrid type-logical grammars, a logic combining Lambek grammars with lambda grammars. We prove some basic properties of the calculus, such as normalisation and the subformula property and also present both a sequent and a proof net calculus for hybrid type-logical grammars. In addition to clarifying the logical foundations of hybrid type-logical grammars, the current study opens the way to variants and extensions of the original system, including but not limited to a non-associative version and a multimodal version incorporating structural rules and unary modes.
MSC:
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 03B40 | Combinatory logic and lambda calculus |
| 03F05 | Cut-elimination and normal-form theorems |
| 03F07 | Structure of proofs |
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Bondy, J. A., & Murty, U. S. R. (2008). Graph theory, Graduate Texts in Mathematics, vol. 244. Springer. · Zbl 1134.05001 |
| [2] | Buszkowski, W., Some decision problems in the theory of syntactic categories, Mathematical Logic Quarterly, 28, 539-548 (1982) · Zbl 0499.03010 · doi:10.1002/malq.19820283308 |
| [3] | Danos, V. (1990). La logique linéaire appliquée à l’étude de divers processus de normalisation (principalement du \(\lambda \)-calcul). Ph.D. thesis, University of Paris VII. |
| [4] | de Groote, P., & Retoré, C. (1996). On the semantic readings of proof nets. In G. J. Kruijff, G. Morrill, R. T. Oehrle (Eds.) Formal grammar, pp. 57-70. |
| [5] | Di Cosmo, R.; Kesner, D., Combining algebraic rewriting, extensional lambda calculi, and fixpoints, Theoretical Computer Science, 169, 201-220 (1996) · Zbl 0874.68158 · doi:10.1016/S0304-3975(96)00121-1 |
| [6] | Emms, M. (1993). Parsing with polymorphism. In Proceedings of the sixth conference of the European association of computational linguistics, pp. 120-129. |
| [7] | Emms, M. (1995). An undecidability result for polymorphic Lambek calculus. In Proceedings of the 10th Amsterdam colloquium. |
| [8] | Girard, JY, Linear logic, Theoretical Computer Science, 50, 1-102 (1987) · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4 |
| [9] | Girard, J. Y., Lafont, Y., & Taylor, P. (1988). Proofs and types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press. · Zbl 0671.68002 |
| [10] | Kanovich, M. I., Kuznetsov, S., & Scedrov, A. (2019). The complexity of multiplicative-additive lambek calculus: 25 years later. In R. Iemhoff, M. Moortgat, R. J. G. B. de Queiroz (Eds.) Logic, language, information, and computation - 26th international workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11541, pp. 356-372. Springer. · Zbl 1530.03091 |
| [11] | Klop, J.; van Oostrom, V.; van Raamsdonk, F., Combinatory reduction systems: Introduction and survey, Theoretical Computer Science, 121, 279-308 (1993) · Zbl 0796.03024 · doi:10.1016/0304-3975(93)90091-7 |
| [12] | Kubota, Y. (2010). (in)flexibility of constituency in japanese in multi-modal categorial grammar with structured phonology. Ph.D. thesis, The Ohio State University. |
| [13] | Kubota, Y., & Levine, R. (2012). Gapping as like-category coordination. Lecture Notes in Computer Science. In D. Béchet & A. Dikovsky (Eds.), Logical aspects of computational linguistics (Vol. 7351, pp. 135-150). Nantes: Springer. · Zbl 1291.03056 |
| [14] | Kubota, Y., & Levine, R. (2013a). Coordination in hybrid type-logical grammar. In Ohio State University working papers in linguistics, vol. 60. Columbus, Ohio. |
| [15] | Kubota, Y., & Levine, R. (2013b). Determiner gapping as higher-order discontinuous constituency. In G. Morrill, M. J. Nederhof (Eds.) Formal grammar, lecture notes in computer science, vol. 8036, pp. 225-241. Springer. |
| [16] | Kubota, Y., & Levine, R. (2015). Against ellipsis: Arguments for the direct licensing of ‘noncanonical’ coordinations. Linguistics and Philosophy,38, 521-576. doi:10.1007/s10988-015-9179-7. |
| [17] | Kubota, Y., & Levine, R. (2020). Type-logical syntax. MIT Press. |
| [18] | Lambek, J., The mathematics of sentence structure, American Mathematical Monthly, 65, 154-170 (1958) · Zbl 0080.00702 · doi:10.1080/00029890.1958.11989160 |
| [19] | Lincoln, P.; Mitchell, J.; Scedrov, A.; Shankar, N., Decision problems for propositional linear logic, Annals of Pure and Applied Logic, 56, 1-3, 239-311 (1992) · Zbl 0768.03003 · doi:10.1016/0168-0072(92)90075-B |
| [20] | Martin, S. (2013). The dynamics of sense and implicature. Ph.D. thesis, The Ohio State University. |
| [21] | Mihaliček, V., & Pollard, C. (2012). Distinguishing phenogrammar from tectogrammar simplifies the analysis of interrogatives. In Formal grammar: FG2010, FG2011, Lecture Notes in Computer Science, vol. 7395, pp. 130-145. Springer. doi:10.1007/978-3-642-32024-8_9 · Zbl 1370.03041 |
| [22] | Mihaličik, V. (2012). Serbo-croatian word order: A logical approach. Ph.D. thesis, The Ohio State University. |
| [23] | Moortgat, M., Categorial investigations: Logical and linguistic aspects of the Lambek calculus (1988), Dordrecht: Foris, Dordrecht · doi:10.1515/9783112329580 |
| [24] | Moortgat, M. (1997). Categorial type logics. In J. van Benthem, A. ter Meulen (Eds.) Handbook of logic and language, chap. 2, pp. 93-177. Elsevier/MIT Press. · Zbl 0874.03001 |
| [25] | Moortgat, M., & Moot, R. (2013). Proof nets for the Lambek-Grishin calculus. In E. Grefenstette, C. Heunen, M. Sadrzadeh (Eds.) Quantum physics and linguistics: A compositional, diagrammatic discourse, pp. 283-320. Oxford University Press. · Zbl 1350.03023 |
| [26] | Moot, R. (2002). Proof nets for linguistic analysis. Ph.D. thesis, Utrecht Institute of Linguistics OTS, Utrecht University. · Zbl 1013.03016 |
| [27] | Moot, R. (2014). Hybrid type-logical grammars, first-order linear logic and the descriptive inadequacy of lambda grammars. Tech. rep.: LaBRI (CNRS), Bordeaux University. |
| [28] | Moot, R.; Puite, Q., Proof nets for the multimodal Lambek calculus, Studia Logica, 71, 3, 415-442 (2002) · Zbl 1013.03016 · doi:10.1023/A:1020525032763 |
| [29] | Moot, R., & Stevens-Guille, S. J. (2019). Proof-theoretic aspects of hybrid type-logical grammars. In Proceedings of formal grammar 2019, Lecture Notes in Computer Science, vol. 11668, pp. 84-100. Springer. · Zbl 1530.03130 |
| [30] | Morrill, G. (1999). Geometry of lexico-syntactic interaction. In Proceedings of the ninth conference of the European chapter of the association for computational linguistics, pp. 61-70. Bergen, Norway. |
| [31] | Muskens, R. (2001). Categorial grammar and lexical-functional grammar. In Proceedings of the LFG01 conference, pp. 259-279. University of Hong Kong. |
| [32] | Newman, M. H. A. (1942). On theories with a combinatorial definition of “equivalence.” Annals of mathematics,43(2), 223-243. · Zbl 0060.12501 |
| [33] | Pentus, M., Lambek calculus is NP-complete, Theoretical Computer Science, 357, 1, 186-201 (2006) · Zbl 1104.03013 · doi:10.1016/j.tcs.2006.03.018 |
| [34] | Perrier, G., A PSPACE-complete fragment of second order linear logic, Theoretical Computer Science, 222, 1-2, 267-289 (1999) · Zbl 0933.03018 · doi:10.1016/S0304-3975(98)00315-6 |
| [35] | Pollard, C., Agnostic hyperintensional semantics, Synthese, 192, 535-562 (2015) · Zbl 1357.03066 · doi:10.1007/s11229-013-0373-2 |
| [36] | Savateev, Y. (2009). Product-free Lambek calculus is NP-complete. In Symposium on logical foundations of computer science (LFCS), pp. 380-394. · Zbl 1211.03041 |
| [37] | Smith, E. A. (2010). Correlational comparison in english. Ph.D. thesis, The Ohio State University. |
| [38] | Worth, C. (2014). The phenogrammar of coordination. In Proceedings of the EACL 2014 workshop on type theory and natural language semantics (TTNLS), pp. 28-36. |
| [39] | Yoshinaka, R., & Kanazawa, M. (2005). The complexity and generative capacity of lexicalized abstract categorial grammars. In Proceedings of logical aspects of computational linguistics 2005, lecture notes in artificial intelligence, vol. 3492, pp. 330-346. Springer, Bordeaux, France. · Zbl 1082.68047 |
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.
