Research Papers & Talks by Stepan Kuznetsov

2020

M. Kanovich, S. Kuznetsov, A. Scedrov. Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities

[full text on arXiv]

• Journal of Logic and Computation, 30:1 (2020), 239--256.

2019

S. Kuznetsov, V. Lugovaya, A. Ryzhova. Craig's trick and a non-sequential system for the Lambek calculus and its fragments

[abstract] [free access link]

Abstract

We show that Craig’s trick is not valid for the Lambek calculus, i.e., there exists such a recursively enumerable theory (set of sequents) over the Lambek calculus, which does not have a decidable axiomatisation. We show that Lambek’s non-emptiness restriction (the constraint that left-hand sides of all sequents should be non-empty) and an infinite set of variables are crucial for the failure of Craig’s trick. We also present a non-sequential formulation of the product-free fragment of the Lambek calculus and show its equivalence to the sequential one.

• Logic Journal of the IGPL, 27:3 (2019), 252–266
• DOI: 10.1093/jigpal/jzy037

M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov. Subexponentials in non-commutative linear logic

[abstract] [preprint on arXiv]

Abstract

Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organised as sets and multisets of formulae not being possible to organise formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.

• Mathematical Structures in Computer Science, 29:8 (2019), 1217–1249
• A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday.
• DOI: 10.1017/S0960129518000117

S. Kuznetsov. The logic of action lattices is undecidable

[abstract] [.pdf]

We prove algorithmic undecidability of the (in)equational theory of residuated Kleene lattices (action lattices), thus solving a problem left open by D. Kozen, P. Jipsen, W. Buszkowski.

• LICS 2019, Vancouver (B. C.), June 24–27, 2019.
• DOI: 10.1109/LICS.2019.8785659

M. Kanovich, S. Kuznetsov, A. Scedrov. The complexity of multiplicative-additive Lambek calculus: 25 years later

[.pdf]

• WoLLIC 2019, Utrecht, July 2–5.
• Springer LNCS vol. 11541, 356–372

M. Kanovich, S. Kuznetsov, A. Scedrov. L-models and R-models for the Lambek calculus enriched with additives and the multiplicative unit

[.pdf]

• WoLLIC 2019, Utrecht, July 2–5.
• Springer LNCS vol. 11541, 373–391

M. Kanovich, S. Kuznetsov, A. Scedrov. Undecidability of a newly proposed calculus for CatLog3

[.pdf]

• Formal Grammar 2019, Riga, August 11
• Springer LNCS vol. 11668, 67–83

2018

S. Kuznetsov. *-continuity vs. induction: divide and conquer

[abstract] [.pdf]

Abstract

The Kleene star can be axiomatised in two ways: inductively, as a fixpoint, or as the ω-iteration of multiplications. The latter is called *-continuity and is stronger than the former: not every Kleene algebra is *-continuous. In the language of only multiplication, union, and Kleene star, however, the (in)equational atomic theory (logic) of *-continuous Kleene algebras coincides with the one of all Kleene algebras (Kozen, 1994). The situation changes dramatically when one adds division operations. As shown by Buszkowski (2007), then the logic with *-continuity becomes \(\Pi_1^0\)-hard and therefore strictly stronger than the inductive one. This result, however, is not constructive, i.e., does not yield a formula distingushing them. Our contribution is threefold. First, we present an example of Kleene algebra with divisions and intersection, which is not *-continuous. Second, we present a formula which makes Buszkowski’s result constructive (see above). Third, we show that the calculus for *-continuity is incomplete w.r.t. more specific relational and language models, in the fragment with divisions, multiplication, intersection, and Kleene star. The choice of this fragment is natural, since union or the unit constant are known to yield incompleteness even without Kleene star.

• AiML 2018, Bern, August 27–31
• Advances in Modal Logic vol. 12, 493–510; College Publications, London
• Editors: G. Bezhanishvili, G. D'Agostino, G. Metcalfe, T. Studer

M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov. A logical framework with commutative and non-commutative subexponentials

[abstract] [.pdf]

Abstract

Logical frameworks allow the specification of deductive systems using the same logical machinery. Linear logical frameworks have been successfully used for the specification of a number of computational, logics and proof systems. Its success relies on the fact that formulas can be distinguished as linear, which behave intuitively as resources, and unbounded, which behave intuitionistically. Commutative subexponentials enhance the expressiveness of linear logic frameworks by allowing the distinction of multiple contexts. These contexts may behave as multisets of formulas or sets of formulas. Motivated by applications in distributed systems and in type-logical grammar, we propose a linear logical framework containing both commutative and non-commutative subexponentials. Non-commutative subexponentials can be used to specify contexts which behave as lists, not multisets, of formulas. In addition, motivated by our applications in type-logical grammar, where the weakenening rule is disallowed, we investigate the proof theory of formulas that can only contract, but not weaken. In fact, our contraction is non-local. We demonstrate that under some conditions such formulas may be treated as unbounded formulas, which behave intuitionistically.

• IJCAR 2018, Oxford, July 14–17
• Springer LNAI vol. 10900, 228–245
• Editors: D. Galmiche, S. Schulz, R. Sebastiani
• The final publication is available at link.springer.com.

G. Morrill, S. Kuznetsov, M. Kanovich, A. Scedrov. Bracket induction for Lambek calculus with bracket modalities

[abstract] [.pdf]

Abstract

Relativisation involves dependencies which, although unbounded, are constrained with respect to certain island domains. The Lambek calculus L can provide a very rudimentary account of relativi- sation limited to unbounded peripheral extraction; the Lambek calculus with bracket modalities Lb can further condition this account according to island domains. However in naı̈ve parsing/theorem-proving by back- ward chaining sequent proof search for Lb the bracketed island domains, which can be indefinitely nested, have to be specified in the linguistic in- put. In realistic parsing word order is given but such hierarchical brack- eting structure cannot be assumed to be given. In this paper we show how parsing can be realised which induces the bracketing structure in backward chaining sequent proof search with Lb.

• Formal Grammar 2018, Sofia, August 11–12
• Springer LNCS vol. 10950, 84–101.
• Editors: A. Foret, G. Kobele, S. Pogodalla.
• The final publication is available at link.springer.com.

S. Kuznetsov. Induction principles in residuated Kleene structures

• Formal Philosophy 2018, Moscow, October 1–2

С. Л. Кузнецов. О полноте фрагмента исчисления Ламбека с операциями итерации и пересечения относительно реляционных моделей

[сборник тезисов]

• Мальцевские чтения 2018, Новосибирск, 19–22 ноября

С. Л. Кузнецов. \(\Pi_1^0\)-полнота исчисления Ламбека с итерацией Клини

[видео на MathNet.ru]

• Традиционная зимняя сессия МИАН–ПОМИ, посвящённая теме «Математическая логика», Москва, 24–25 декабря 2018 г.

С. Л. Кузнецов. Звёздочка Клини в частично упорядоченных структурах с делением

• DDA 2018, Москва, 27–28 декабря

2017

M. Kanovich, S. Kuznetsov, A. Scedrov. Undecidability of the Lambek calculus extended with subexponential and bracket modalities

[extended version on arXiv]

• FCT 2017, Bordeaux, September 11–13
• Springer LNCS vol. 10472, 326–340
• Editors: R. Klasing, M. Zeitoun
• The final publication is available at link.springer.com.
• Extended text on arXiv updated on May 4, 2017.

M. Kanovich, S. Kuznetsov, G. Morrill, A. Scedrov. A polynomial time algorithm for the Lambek calculus with brackets of bounded order

[abstract] [full text]

Abstract

Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. Pentus (2010) gave a polynomial-time algorithm for determining provability of bounded depth formulas in L*, the Lambek calculus with empty antecedents allowed. Pentus' algorithm is based on tabularisation of proof nets. Lambek calculus with brackets is a conservative extension of Lambek calculus with bracket modalities, suitable for the modeling of syntactical domains. In this paper we give an algorithm for provability in Lb*, the Lambek calculus with brackets allowing empty antecedents. Our algorithm runs in polynomial time when both the formula depth and the bracket nesting depth are bounded. Our algorithm combines a Pentus-style tabularisation of proof nets, together with an automata-theoretic treatment of bracketing.

• FSCD 2017, Oxford, September 3–9
• Leibniz International Proceedings in Informatics (LIPIcs) vol. 84, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 22:1–22:17.
• Editor: D. Miller

S. Kuznetsov. The Lambek calculus with iteration: two variants.

[abstract] [full text on arXiv]

Abstract

Formulae of the Lambek calculus are constructed using three binary connectives, multiplication and two divisions. We extend it using a unary connective, positive Kleene iteration. For this new operation, following its natural interpretation, we present two lines of calculi. The first one is a fragment of infinitary action logic and includes an omega-rule for introducing iteration to the antecedent. We also consider a version with infinite (but finitely branching) derivations and prove equivalence of these two versions. In Kleene algebras, this line of calculi corresponds to the *-continuous case. For the second line, we restrict our infinite derivations to cyclic (regular) ones. We show that this system is equivalent to a variant of action logic that corresponds to general residuated Kleene algebras, not necessarily *-continuous. Finally, we show that, in contrast with the case without division operations (considered by Kozen), the first system is strictly stronger than the second one. To prove this, we use a complexity argument. Namely, we show, using methods of Buszkowski and Palka, that the first system is \(\Pi _1^0\)-hard, and therefore is not recursively enumerable and cannot be described by a calculus with finite derivations.

• WoLLIC 2017, London, July 18–21
• Springer LNCS vol. 10388, 182–198
• Editors: J. Kennedy, R. de Queiroz
• The final publication is available at link.springer.com

S. Kuznetsov, A. Okhotin. Conjunctive categorial grammars

[abstract] [full text, .pdf]

Abstract

Basic categorial grammars are enriched with a conjunction operation, and it is proved that the formalism obtained in this way has the same expressive power as conjunctive grammars, that is, context-free grammars enhanced with conjunction. It is also shown that categorial grammars with conjunction can be naturally embedded into the Lambek calculus with conjunction and disjunction operations. This further implies that a certain NP-complete set can be defined in the Lambek calculus with conjunction.

• Mathematics of Language 2017, London, July 13–14
• ACL Anthology, W17-3414
• Editors: M. Kanazawa, Ph. de Groote, M. Sadrzadeh

S. Kuznetsov, G. Morrill, O. Valentín. Count-invariance including exponentials

[abstract] [full text, .pdf]

Abstract

We define infinitary count-invariance for categorial logic, extending countinvariance for multiplicatives (van Benthem, 1991) and additives and bracket modalities (Valentín et al., 2013) to include exponentials. This provides an effective tool for pruning proof search in categorial parsing/theorem-proving.

• Mathematics of Language 2017, London, July 13–14
• ACL Anthology, W17-3413
• Editors: M. Kanazawa, Ph. de Groote, M. Sadrzadeh

S. Kuznetsov, V. Lugovaya, A. Ryzhova. Recursive enumerability doesn't always give a decidable axiomatization

[.pdf]

• TbiLLC 2017, Lagodekhi, Georgia, September 18–22

S. Kuznetsov. Iteration in residuated structures

[abstract] [video on MathNet.ru]

Abstract

We consider residuated semigroups, i.e., partially ordered semigroups with division operations, enriched with the positive iteration operation ( an analog of Kleene star, but with the non-emptiness condition). There are two ways for defining iteration: by induction and by *-continuity; a standard example for the second approach is the powerset of the free semigroup a.k.a. the algebra of formal languages (without the empty word). We show that the atomic inequational theories for these two approaches differ. Note that for the non-residuated case the situation is different: as shown by Kozen, equational theories of Kleene algebras and the subclass of *-continuous Kleene algebras coincide. The proof is non-constructive and is based on complexity considerations: we show that the calculus for the *-continuous case, which is the Lambek calculus extended with infinitary rules for the iteration, has a \(\Pi_1^0\)-complete derivability problem (we show it using methods by Buszkowski and Palka), and for the inductive system we have a circular proof system, which is definitely recursively enumerable. We also consider the Lambek calculus extended both with iteration and the (sub)exponential modality allowing the contraction rule (in the non-local form) and show that the complexity there is at least \(\Pi_1^1\). Finally, we raise some open questions for future research, both technical (probably easy to solve, like translating the results from semigroups with positive iteration to monoids with Kleene iteration etc.) and significant (most importantly, completeness w.r.t. models on formal languages).

• Wormshop 2017 (4th International Workshop on Proof Theory, Modal Logic and Reflection Principles), Steklov Mathematical Institute, Moscow, October 17–20.
• PC: L. Beklemishev, D. Fernández Duque, J. Joosten, F. Pakhomov.

S. Kuznetsov. Iteration in residuated structures

[abstract] [video on YouTube]

Abstract

We present a system with infinite derivations axiomatising the elementary theory of *-continuous Kleene algebras with divisions (residuated Kleene algebras) and show that its circular fragment axiomatises the elementary theory of arbitrary residuated Kleene algebras. In contrast with the nonresiduated case, where these theories coincide (as shown by Kozen), here the infinitary one happens to be not recursively enumerable, and therefore properly includes the circular one.

• Workshop “Constructive Knowledge — 4: Epistemic Logics and the Problem of Jusification”, Institute of Philosophy, RAS, Moscow, November 15.

S. Kuznetsov. Eliminating the unit constant in the Lambek calculus with brackets

[abstract] [full text on arXiv]

Abstract

We present a translation of the Lambek calculus with brackets and the unit constant, \(\mathbf{Lb}^*_{\mathbf{1}}\), into the Lambek calculus with brackets allowing empty antecedents, but without the unit constant, \(\mathbf{Lb}^*\). Using this translation, we extend previously known results for \(\mathbf{Lb}^*\) to \(\mathbf{Lb}^*_{\mathbf{1}}\): (1) languages generated by categorial grammars based on the Lambek calculus with brackets are context-free (Kanazawa 2017); (2) the polynomial-time algorithm for deciding derivability of bounded depth sequents (Kanovich et al. 2017).

2016

С. Л. Кузнецов. О преобразовании грамматик Ламбека с одним делением в контекстно-свободные грамматики.

[аннотация] [полный текст, .pdf]

Аннотация

В работе описан способ построения по грамматике Ламбека с одним делением контекстно-свободной грамматики, задающей тот же язык, размер которой ограничен полиномом от размера исходной грамматики. Известные ранее конструкции Бушковского и Пентуса приводили к экспоненциальному росту размера грамматики.

• Труды МИАН, 294, 2016, 141–151.
• Сайт издателя: http://www.maik.ru/

S. L. Kuznetsov. On translating Lambek grammars with one division into context-free grammars.

[full text, .pdf]

• Proc. Steklov Inst. Math., 294, 2016, 129--138.

M. Kanovich, S. Kuznetsov, A. Scedrov. Undecidability of the Lambek calculus with a relevant modality

[full text on arXiv]

Formal Grammar 2016, Bolzano/Bozen, August 20–21.

Springer LNCS vol. 9804 (joint proceedings of Formal Grammar 2015 and 2016), 240–256.

Editors: A. Foret, G. Morrill, R. Muskens, R. Osswald, S. Pogodalla.

The final publication is available at link.springer.com.

M. Kanovich, S. Kuznetsov, A. Scedrov. On Lambek's restriction in the presence of exponential modalities

• LFCS 2016, Deerfield Beach, Florida, January 4–7.
• Springer LNCS vol. 9537, 146–158.

S. Kuznetsov. On the Lambek calculus with the Kleene star and the exponential

[abstract] [.pdf]

Abstract

We introduce an infinitary extension of the Lambek calculus with the Kleene star and the linear logic exponential modality. For this system we establish cut elimination and some other properties and also prove that, due to complexity reasons, it cannot be replaced by a system with finite proofs.

• AiML 2016 (short paper), Budapest, August 30 – September 2.

S. Kuznetsov. The Lambek calculus with unary connectives

[.pdf]

(partially based on joint work with M. Kanovich, A. Scedrov, and N. Ryzhkova)

• Logic and Applications 2016, Dubrovnik, September 19–23, 2016.

M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov. On the proof theory of non-commutative subexponentials

[abstract] [.pdf]

Abstract

Linear logical frameworks with subexponentials have been used for the specification of among other systems, proof systems, concurrent programming languages and linear authorization logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organized as sets and multisets of formulae not being possible to organize formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut-elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with local and non-local contraction rules. We also obtain some new undecidability results on non-commutative linear logic with subexponentials.

• Dale Fest!^60th (seminar in honor of the 60th birthday of Dale Miller), Paris, December 15–16, 2016.
• Organisers: D. Baelde, A. Felty, G. Nadathur, V. Nigam, A. Saurin.

2015

С. Л. Кузнецов. О преобразовании контекстно-свободных грамматик в грамматики Ламбека

• Труды МИАН, 290, 2015, 72–79.

S. L. Kuznetsov. On translating context-free grammars into Lambek grammars

• Proc. Steklov Inst. Math., 290, 2015, 63–69.

С. Л. Кузнецов, Н. С. Рыжкова. Фрагмент исчисления Ламбека с итерацией

[сборник тезисов]

• Мальцевские чтения 2015, Новосибирск, 3–7 мая

2014

S. Kuznetsov. Trivalent logics arising from L-models for the Lambek calculus with constants

• Journal of Applied Non-Classical Logics, 14:1–2 (2014), 132–137.

S. Kuznetsov. L-completeness of the Lambek calculus with the reversal operation allowing empty antecedents.

[abstract] [full text, .pdf]

Abstract

In this paper we prove that the Lambek calculus allowing empty antecedents and enriched with a unary connective corresponding to language reversal is complete with respect to the class of models on subsets of free monoids (L-models).

• Categories and Types in Logic, Language, and Physics. Essays dedicated to Jim Lambek on the occasion of his 90th birthday
• Springer LNCS vol. 8222, 268– 278
• Editors: C. Casadio, B. Coecke, M. Moortgat, Ph. Scott
• The final publication is available at link.springer.com.

S. Kuznetsov. On translating context-free grammars into Lambek categorial grammars

[proceedings as techreport, .pdf]

• NLCS 2014 (at VSL 2014), Vienna, July 17–18, 2014.
• Proceedings published (jointly with NLSR 2014) as a technical report, Center for Informatics and Systems, University of Coimbra, Portugal.
• Editors: V. de Paiva, W. Neuper, P. Quaresma, C. Retoré, L. S. Moss, J. Saludes.

2013

S. Kuznetsov. Conjunctive grammars in Greibach normal form and the Lambek calculus with additive connectives

[full text, .pdf]

• Formal Grammar 2013, Düsseldorf, August 10–11.
• Spinger LNCS vol. 8036 (joint proceedings of Formal Grammar 2012 and 2013), 242–249.
• Editors: G. Morrill, M.-J. Nederhof.
• The final publication is available at link.springer.com.

С. Л. Кузнецов. Об исчислении Ламбека с операцией пересечения и конъюнктивных грамматиках

[сборник тезисов]

• Мальцевские чтения 2013, Новосибирск, 11–15 ноября.

2012

С. Л. Кузнецов. Категориальные грамматики, основанные на вариантах исчисления Ламбека (канд. дисс.)

[автореферат, .pdf] [полный текст, .pdf]

Unofficial translation: S. L. Kuznetsov. Categorial grammars based on variants of the Lambek calculus (C. Sc. Thesis)

[summary, .pdf] [full text, .pdf]

S. Kuznetsov. Lambek grammars with one division and one primitive type

• Logic Journal of the IGPL, 20:1 (2012), 207–221.
• DOI: 10.1093/jigpal/jzr031
• This paper is incorporated into the C. Sc. thesis, Chapter 3 and Section 1.8.

S. Kuznetsov. L-completeness of the Lambek calculus with the reversal operation

[abstract] [full text, .pdf]

Abstract

We extend the Lambek calculus with rules for a unary operation corresponding to language reversal and prove that this calculus is complete with respect to the class of models on subsets of free semigroups (L-models). We also prove that categorial grammars based on this calculus generate precisely all context-free languages without the empty word.

• LACL 2012, Nantes, June 2–4
• Springer LNCS vol. 7351, 151–160
• Editors: D. Béchet, A. Dikovsky
• The final publication is available at link.springer.com.
• This paper is incorporated into the C. Sc. thesis, Chapter 4.

Препринт по-русски: С. Л. Кузнецов. Исчисление Ламбека с операцией обращения

[.pdf]

• Депонировано в ВИНИТИ 17.04.2012, № 152–В2012.

S. Kuznetsov. Lambek grammars with the unit

• Formal Grammar 2011, Ljubljana, August 6–7, 2011.
• Springer LNCS vol. 7395 (joint proceedings of Formal Grammar 2010 and 2011, published in 2012), 262–266.
• Editors: Ph. de Groote, M.-J. Nederhof.
• DOI: 10.1007/978-3-642-32024-8_17.
• This paper is incorporated into the C. Sc. thesis, Section 2.2.

С. Л. Кузнецов. Исчисление Ламбека с операцией обращения

[аннотация, .pdf]

• Московские чтения по конструктивной логике и представлению знаний к 60-летию С. Н. Артёмова, Москва, 30–31 мая 2012 г.
• Оргкомитет: Л. Д. Беклемишев, В. Б. Шехтман, Т. Л. Яворская

S. Kuznetsov. Grammars based on variants of the Lambek calculus

[abstract] [video on MathNet.ru]

Abstract

We consider the Lambek calculus with one division and one primitive type (\(\mathrm{L}(\backslash;p)\)) and two extensions of the Lambek calculus: \(\mathrm{L}_1\) (adding the unit constant) and \(\mathrm{L}^{\mathrm{R}}\) (adding a unary connective that corresponds to taking the language of the inverse strings). We prove that (\(\mathrm{L}(\backslash;p)\))-grammars and \(\mathrm{L}^{\mathrm{R}}\)-grammars generate precisely all context-free languages without the empty word, and \(\mathrm{L}_1\)-grammars generate precisely all context-free languages.

• LMRC 2012, Moscow, February 1–3.
• PC: M. Baaz, L. Beklemishev, Y. Gurevich.

S. Kuznetsov. Trivalent logics arising from L-models for the Lambek calculus with constants

[workshop proceedings, .pdf]

• Workshop on Three-valued Logics and their Applications (at ESSLLI 2012), Opole, August 13–17, 2012.
• Selected papers were published in a special issue of JANCL.

С. Л. Кузнецов. Об исчислении Ламбека с операцией обращения

[сборник тезисов]

• Мальцевские чтения 2012, Новосибирск, 12–16 ноября.

2011

С. Л. Кузнецов. Об исчислении Ламбека с единицей и одним делением

• Вестник Московского университета. Серия 1. Математика, механика. 2011, № 4, 55–57.
• Эта статья включена в кандидатскую диссертацию, раздел 2.3.

S. L. Kuznetsov. On the Lambek calculus with a unit and one division

• Moscow University Mathematics Bulletin, 66:4 (2011), 173–175.
• DOI: 10.3103/S0027132211040085
• This paper is incorporated into the C. Sc. thesis, Section 2.3.

2009

С. Л. Кузнецов. Об исчислении Ламбека с одним делением и одним примитивным типом, допускающим пустые антецеденты

• Вестник Московского университета. Серия 1. Математика, механика. 2009, № 2, 62–65.
• Эта статья включена в кандидатскую диссертацию, глава 3.

S. L. Kuznetsov. On the Lambek calculus with one division and one primitive type allowing empty antecedents

• Moscow University Mathematics Bulletin, 64:2 (2009), 76–79.
• DOI: 10.3103/S0027132209020089
• This paper is incorporated into the C. Sc. thesis, Chapter 3.

S. Kuznetsov. On the Lambek calculus with one division and one primitive type

[abstract] [workshop proceedings, .pdf]

Abstract

The following theorem is proved: a formal language without the empty word is context-free if and only if it is generated by some \(\mathrm{L}(\backslash;p_1)\)-grammar, where \(\mathrm{L}(\backslash;p_1)\) is the Lambek calculus with one division and one primitive type. To do that, we use a substitution of types which reduces derivability in \(\mathrm{L}(\backslash)\) to derivability \(\mathrm{L}(\backslash;p_1)\).

• Workshop “Structures and Deduction” (at ESSLLI 2009), Bordeaux, July 20–24.
• Editors: M. Parigot, L. Straßburger