A restricted fragment of the Lambek calculus with iteration and intersection operations

S. L. Kuznetsov ; N. S. Ryzhkova

Algebra i logika, Tome 59 (2020) no. 2, pp. 190-214.

Résumé

The Lambek calculus (a variant of intuitionistic linear logic initially introduced for mathematical linguistics) enjoys natural interpretations over the algebra of formal languages ($\mathrm{L}$-models) and over the algebra of binary relations which are subsets of a given transitive relation (R-models). For both classes of models there are completeness theorems (Andréka and Mikulás [J. Logic Lang. Inf., 3, No. 1 (1994), 1—37]; Pentus [Ann. Pure Appl. Logic, 75, Nos. 1/2 (1995), 179—213; Fund. Prikl. Mat., 5, No. 1 (1999), 193—219]). The operations of the Lambek calculus include product and two divisions, left and right. We consider an extension of the Lambek calculus with intersection and iteration (Kleene star). It is proved that this extension is incomplete both w.r.t. $\mathrm{L}$-models and w.r.t. $\mathrm{R}$-models. We introduce a restricted fragment, in which iteration is allowed only in denominators of division operations. For this fragment we prove completeness w.r.t. $\mathrm{R}$-models. We also prove completeness w.r.t. $\mathrm{L}$-models for the subsystem without product. Both results are strong completeness theorems, that is, they establish equivalence between derivability from sets of hypotheses (finite or infinite) and semantic entailment from sets of hypotheses on the given class of models. Finally, we prove $\Pi_1^0$-completeness of the algorithmic problem of derivability in the restricted fragment in question.

Détail

Mots-clés : Lambek calculus
Keywords: Kleene iteration, algebra of formal languages, algebra of binary relations, complexity of derivability problem.

Bibliographie

[1] J. Lambek, “The mathematics of sentence structure”, Amer. Math. Mon., 65 (1958), 154–170 ; I. Lambek, “Matematicheskoe issledovanie struktury predlozhenii”, Matematicheskaya lingvistika, sb. per. pod. red. Yu. A. Shreidera i dr., Mir, M., 1964, 47–68 | MR | Zbl

[2] G. Takeuti, Proof theory, Stud. Logic Found. Math., 81, North-Holland Publ. Co., Amsterdam–Oxford, New York, 1975 ; G. Takeuti, Teoriya dokazatelstv, Mir, M., 1978 | MR

[3] V. M. Abrusci, “A comparison between Lambek syntactic calculus and intuitionistic linear propositional logic”, Z. Math. Logik Grundlagen Math., 36:1 (1990), 11–15 | MR | Zbl

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

[5] K. Ajdukiewicz, “Die syntaktische Konnexität”, Stud. Philos., 1 (1935), 1–27

[6] Y. Bar-Hillel, “A quasi-arithmetical notation for syntactic description”, Language, 29 (1953), 47–58 | Zbl

[7] R. Moot, C. Retoré, The logic of categorial grammars. A deductive account of natural language syntax and semantics, Lect. Notes Comput. Sci., 6850, Springer, Berlin, 2012 | MR | Zbl

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

[9] M. Pentus, “Models for the Lambek calculus”, Ann. Pure Appl. Logic, 75:1/2 (1995), 179–213 | MR | Zbl

[10] M. R. Pentus, “Polnota sintaksicheskogo ischisleniya Lambeka”, Fundament. i prikl. matem., 5:1 (1999), 193–219 | MR | Zbl

[11] W. Buszkowski, “Lambek calculus and substructural logics”, Linguist. Analysis, 36:1–4 (2010), 15–48

[12] W. Buszkowski, “Compatibility of a categorial grammar with an associated category system”, Z. Math. Logik Grundlagen Math., 28 (1982), 229–238 | MR | Zbl

[13] S. Kuznetsov, V. Lugovaya, A. Ryzhova, “Craig's trick and a non-sequential system for the Lambek calculus and its fragments”, Log. J. IGPL, 27:3 (2019), 252–266 | MR | Zbl

[14] H. Andréka, Sz. Mikulás, “Lambek calculus and its relational semantics: completeness and incompleteness”, J. Logic Lang. Inf., 3:1 (1994), 1–37 | MR

[15] S. C. Kleene, “Representation of events in nerve nets and finite automata”, Automata studies, Ann. Math. Stud., 34, eds. C. E. Shannon, J. McCarthy, Princeton Univ. Press, Princeton–New Jersey, 1956, 3–41 | MR

[16] W. Buszkowski, “On action logic: equational theories of action algebras”, J. Log. Comput., 17:1 (2007), 199–217 | MR | Zbl

[17] E. Palka, “An infinitary sequent system for the equational theory of *-continuous action lattices”, Fundam. Inform., 78:2 (2007), 295–309 | MR | Zbl

[18] S. Kuznetsov, “*-continuity vs. induction: divide and conquer”, AiML 2018, Proc. 12th conf. (Bern, Switzerland, August 27–31, 2018), Advances in modal logic, 12, eds. G. Bezhanishvili et al., College Publ., London, 2018, 493–510 | MR | Zbl

[19] H. Ono, Y. Komori, “Logics without contraction rule”, J. Symb. Log., 50:1 (1985), 169–201 | MR | Zbl

[20] I. Sedlár, “Iterative division in the distributive full non-associative Lambek calculus”, Dynamic logic. New trends and applications, Second int. workshop DALI 2019 (Porto, Portugal, October 7–11, 2019), Lect. Notes Comput. Sci., 12005, eds. L. S. Barbosa, A. Baltag, Springer, Cham, 2020, 141–154 | Zbl

[21] M. Kanovich, S. Kuznetsov, A. Scedrov, “$\mathrm{L}$-models and $\mathrm{R}$-models for Lambek calculus enriched with additives and the multiplicative unit”, Logic, language, information, and computation, 26th int. workshop WoLLIC 2019 (Utrecht, The Netherlands, July 2–5, 2019), Lect. Notes Comput. Sci., 11541, eds. R. Iemhoff et al., Springer, Berlin, 2019, 373–391 | MR | Zbl

[22] S. Kuznetsov, “The Lambek calculus with iteration: two variants”, Logic, language, information, and computation, 24th int. workshop WoLLIC 2017 (London, UK, July 18–21, 2017), Lect. Notes Comput. Sci., 10388, eds. J. Kennedy et al., Springer, Berlin–Heidelberg, 2017, 182–198 | MR | Zbl

[23] Y. Bar-Hillel, C. Gaifman, E. Shamir, “On categorial and phrase-structure grammars”, Bull. Res. Council. Israel, Sect. F, 9F (1960), 1–16 | MR

[24] W. Buszkowski, “The equivalence of unidirectional Lambek categorial grammars and context-free grammars”, Z. Math. Logik Grundlagen Math., 31 (1985), 369–384 | MR | Zbl

[25] M. Pentus, “Lambek grammars are context-free”, Proc. 8th IEEE Symp. Logic in Comput. Sci., 1993, 429–433 | MR

[26] M. R. Pentus, “Ischislenie Lambeka i formalnye grammatiki”, Fundament. i prikl. matem., 1:3 (1995), 729–751 | MR | Zbl

[27] M. Pentus, “Product-free Lambek calculus and context-free grammars”, J. Symb. Log., 62:2 (1997), 648–660 | MR | Zbl

[28] D. Kozen, “On the complexity of reasoning in Kleene algebra”, Inf. Comput., 179:2 (2002), 152–162 | MR | Zbl

[29] V. Pratt, “Action logic and pure induction”, Logics in AI, European workshop JELIA '90 (Amsterdam, Netherlands, September 10-14, 1990), Lect. Notes Comput. Sci., 478, ed. J. van Eijck, Springer-Verlag, Berlin etc., 1991, 97–120 | MR | Zbl

[30] D. Kozen, “On action algebras”, Logic and information flow, MIT Press Ser. Found. Comput., eds. J. van Eijck, A. Visser, MIT Press, Cambridge, MA, 1994, 78–88 | MR

[31] A. Das, D. Pous, “Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)”, 27th EACSL Annual Conf. Comput. Sci. Logic CSL 2018 (Birmingham, UK, 4–7 September 2018), 2018, 19:1–19:18 | MR | Zbl

[32] S. Kuznetsov, “The logic of action lattices is undecidable”, 34th Annual ACM/IEEE Symp. Logic in Comput. Sci. (LICS) (Vancouver, BC, Canada, 2019), 1–9 | DOI | MR