The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities
- PDF / 889,418 Bytes
- 58 Pages / 439.37 x 666.142 pts Page_size
- 95 Downloads / 161 Views
The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities Max Kanovich1,2 · Stepan Kuznetsov2,3
· Andre Scedrov4,5
Accepted: 29 September 2020 © Springer Nature B.V. 2020
Abstract 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 both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut (cut elimination theorem). We also prove algorithmic undecidability for both calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages. Keywords Lambek calculus · Categorial grammars · Subexponential modalities · Bracket modalities · Undecidability · cut elimination Mathematics Subject Classification 03B47 · 03F52 · 03F05 · 03D03 · 03D25
B
Stepan Kuznetsov [email protected] Max Kanovich [email protected] Andre Scedrov [email protected]
1
University College London, Gowers St., London, UK
2
Steklov Mathematical Institute of the Russian Academy of Sciences, 8 Gubkina St., Moscow, Russia
3
National Research University Higher School of Economics, 11 Pokrovsky Blvd., Moscow, Russia
4
University of Pennsylvania, 209 South 33rd St., Philadelphia, PA, USA
5
National Research University Higher School of Economics (until July 2020), 11 Pokrovsky Blvd., Moscow, Russia
123
M. Kanovich et al.
1 Linguistic Introduction The Lambek calculus (Lambek 1958) was introduced for mathematical modelling of natural language syntax via categorial grammars. The concept of categorial grammar goes back to ideas of Ajdukiewicz (1935) and Bar-Hillel (1953). The framework of categorial grammars aims to describe natural language by means of logical derivability (see Buszkowski (2003), Carpenter (1997), Morrill (2011), Moot and Retoré (2012) etc). From the modern logical point of view, the calculus of Lambek grammars (the Lambek calculus) is a variant of Girard’s linear logic (Girard 1987) in its non-commutative intuitionistic version (Abrusci 1990). Nowadays Lambek-style categorial grammars form one framework in a family of closely related formalisms, including combinatory categorial grammars (Steedman 2000), categorial dependency grammars (Dekhtyar and Dikovsky 2008), and others. A categorial grammar assigns logical formulae to lexemes (words) of the language. These formulae are syntactic categories, or types, of these words. In Lambek grammars, types are constructed using three binary connectives, namely two divisions, \ and /, and the product, ·. Following the usual introduction into categorial grammars, we start with the standard example: “John loves Mary.” Here “John” and “Mary” receive syntactic type N (noun); “loves,” as a transitive
Data Loading...
