The Complexity of Multiplicative-Additive Lambek Calculus: 25 Years Later

Abstract

The Lambek calculus was introduced as a mathematical description of natural languages. The original Lambek calculus is NP-complete (Pentus), while its product-free fragment with only one implication is polynomially decidable (Savateev). We consider Lambek calculus with the additional connectives: conjunction and disjunction. It is known that this system is PSPACE-complete (Kanovich, Kanazawa). We prove, in contrast with the polynomial-time result for the product-free Lambek calculus with one implication, that the derivability problem is still PSPACE-complete even for a very small fragment $(\mathop {\backslash }, \wedge )$, including one implication and conjunction only. PSPACE-completeness is also provided for the $(\mathop {\backslash }, \vee )$ fragment, which includes only one implication and disjunction. Categorial grammars based on the original Lambek calculus generate exactly the class of context-free languages (Gaifman, Pentus). The class of languages generated by Lambek grammars extended with conjunction is known to be closed under intersection (Kanazawa), and therefore includes all finite intersections of context-free languages and, moreover, images of such intersections under alphabetic homomorphisms. We show that the same closure under intersection holds for Lambek grammars extended with disjunction, even for our small $(\mathop {\backslash }, \vee )$ fragment.

Appendices

A PSPACE-completeness of the fragment $\mathcal{L}(\backslash , \vee )$

In this section we will modify Sect. 2 to establish PSPACE-completeness for the fragment $\mathcal{L}(\backslash ,\, \vee \,)$, which includes only one implication and disjunction.

Remark 4

For the sake of readability, we conceive of the formula ${((A \cdot \,B) \backslash \, C)}$ as abbreviation for ${(B \backslash \, {(A \backslash \, C)})}$. In particular, $(A \cdot \,B)^{b}$ is abbreviation for ${(B \backslash \, {(A \backslash \, b)})}$. Because of Lemma 1, the formula $(A^b\wedge B^b)$ is conceived of as abbreviation for ${((A\vee B) \backslash \, b)}$ within this section.

Theorem 4

The fragment $\mathcal{L}(\backslash , \vee )$ is PSPACE-complete.

Proof Sketch. We start with the equality (2), assuming that $\alpha _1$, $\alpha _2$, ..., $\alpha _{2n-1}$, $\alpha _{2n}$ are given.

To prove Lemma 14, the “disjunction analog” of Lemma 3, we modify the basic material given in the “conjunction” Definition 3 by means of Definitions 6 and 7 working within the $\mathcal{L}(\backslash , \vee )$ fragment.

Definition 6

For $1\le i\le 2n$, let $E_{\ell ,i,\beta }$ denote the formula: $(c_{\ell ,i} \backslash \, {(\beta \backslash \, c_{\ell ,i-1})})$.

Let $F_{\ell }$ denote: $(q_{2n} \backslash \, c_{\ell ,2n})$, and $H_{\ell }$ denote: $(c_{\ell ,0} \backslash \, {(e_0 \backslash \, e_0)})$.

Lemma 13

The following “verifying” sequent is derivable in Lambek calculus

$$e_0, \alpha _1, \alpha _2, \dots , \alpha _{2n}, q_{2n}, F_{\ell }, E_{\ell ,2n,\alpha _{2n}}, E_{\ell ,2n-1,\alpha _{2n-1}}, \dots E_{\ell ,2,\alpha _{2}}, E_{\ell ,1,\alpha _{1}}, H_{\ell }\ \vdash \ e_0 $$

Proof

By the inverse induction on i: $\alpha _{i-1}, \alpha _{i}, c_{\ell ,i},\, E_{\ell ,i,\alpha _{i}} \ \vdash \ (\alpha _{i-1} \cdot \,\, c_{\ell ,i-1})$

Definition 7

We introduce the following formulas:

$$\begin{aligned} \left\{ \begin{array}{c}{} \displaystyle { \widetilde{F} = \biggl (\bigvee _{\ell =1}^{m} (F_{\ell })^{b}\biggr )^{b} }, \quad \displaystyle { \widetilde{H} = \biggl (\bigvee _{\ell =1}^{m} (H_{\ell })^{b}\biggr )^{b} } \\[2ex] \displaystyle { \widetilde{E_{i}} = \biggl (\bigvee _{1\le \ell \le m,\ E_{\ell ,i,\beta }\in \mathcal{E}_{\ell ,i}} (E_{\ell ,i,\beta })^{b}\biggr )^{b} } \end{array}\right. \end{aligned}$$

(32)

where a one- or two-element set of formulas, $\mathcal{E}_{\ell ,i}$, is defined as follows:

• (1) $\mathcal{E}_{\ell ,i} = \{\, E_{\ell ,i,t_i}\, \}$, if the conjunct $C_\ell$ contains the variable $x_i$,

• (2) $\mathcal{E}_{\ell ,i} = \{\, E_{\ell ,i,f_i}\, \}$, if the conjunct $C_\ell$ contains $\lnot x_i$,

• (3) $\mathcal{E}_{\ell ,i} = \{\, E_{\ell ,i,t_i},\ E_{\ell ,i,f_i}\, \}$, if $C_\ell$ contains neither $x_i$, nor $\lnot x_i$.

By applying (2) and Lemma 1, we get the desired verification:

Lemma 14

The following sequent is derivable in Lambek

$$e_0^{bb}, \alpha _1^{bb}, \alpha _2^{bb}, \dots , \alpha _{2n-1}, (\alpha _{2n}\cdot \,\, q_{2n})^{bb},\ \varDelta _{n}\ \vdash \ e_0^{bb} $$

where $\varDelta _{n}$ is a sequence of formulas: $\varDelta _{n} = \widetilde{F}, \widetilde{E}_{2n}, \widetilde{E}_{2n-1}, \dots , \widetilde{E_{2}}, \widetilde{E_{1}}, \widetilde{H}$

Corollary 6

It suffices to follow the line of reasoning in Sect. 2 to find appropriate $G_1$, $G_2$, ..., $G_{2n-1}$, $G_{2n}$, such that the following sequent is derivable in Lambek calculus if and only if the statement (1) is valid:

$$\begin{aligned} (e_0^{[4n]}\cdot \,q_0)^{[2]}, G_1^{[2]}, G_2^{[4]}, \dots , G_{2n-1}^{[4n-2]}, G_{2n}^{[4n]}, \ \varDelta _{n}^{[4n]}\ \vdash \ e_0^{[4n+2]} \end{aligned}$$

(33)

B Proofs of Technical Lemmas for Section 3

Proof

(of Lemma 8). Induction on derivation. The sequent in question could not be an axiom, since the antecedent of $F_1 \vee F_2 \vdash F_1 \vee F_2$ includes $F_1 \vee F_2$ in a strictly positive position. Consider the last rule applied in the derivation. It could be $\mathbf {L} {\mathop {\backslash }}$, $\mathbf {L} {\mathop {/}}$, $\mathbf {L} \cdot$, or . Rules with $\wedge$ cannot be used, since there are no $\wedge$’s in the antecedent, and the main connective of the succedent is $\vee$. If the last rule is , we immediately reach our goal.

If the derivation ends with an application of $\mathbf {L} {\cdot }$:

then we apply the induction hypothesis, get $E_1, \ldots , E'_i, E''_i, \ldots , E_n \vdash F_i$ ($i = 1$ or 2) and apply $\mathbf {L} {\cdot }$ to this sequent, which yields our goal.

For $\mathbf {L} {\mathop {\backslash }}$, we get the following

and notice that the antecedent of the right premise still satisfies the conditions of the lemma, thus we can apply induction hypothesis. The induction hypothesis yields $E_1, \ldots , E_i, E''_j, \ldots , E_n \vdash F_i$. Applying $\mathbf {L} {\mathop {/}}$ with the same left premise, $E_{i+1}, \ldots , E_{j-1} \vdash E'_j$, yields our goal.

The $\mathbf {L} {\mathop {/}}$ case is symmetric.

Proof

(of Lemma 9). Induction on derivation. The axiom should be of the form $b \vdash b$, which violates the condition. For each inference rule, we apply the induction hypothesis for the premise from which the succedent b comes.

Proof

(of Lemma 10). Induction on derivation. Induction base is axiom $b \vdash b$. Consider the last rule applied. If it is one of the one-premise rules, then we use the induction hypothesis for the only premise. For applications of $\mathbf {L}{\mathop {/}}$ or $\mathbf {L}{\mathop {\backslash }}$, if the rightmost occurrence of b goes to the right premise, we again directly use the induction hypothesis. Notice that for $\mathbf {L}{\mathop {\backslash }}$ this is always the case. The other rule, $\mathbf {L}{\mathop {/}}$, however, can decompose one of the $F_i$ and take the rightmost b to the left premise:

The right premise, however, now is not derivable by Lemma 9. Contradiction.

Proof

(of Lemma 11). Induction on derivation again. Any one-premise rule applied for one of the $F_i$, as well as $\mathbf {L} {\mathop {/}}$ or $\mathbf {L} {\mathop {\backslash }}$ which keeps $E_k \mathop {\backslash }b$ in the right premise, is handled by directly using the induction hypothesis and applying the same rule. The situation where $\mathbf {L} {\mathop {/}}$ takes $E_k \mathop {\backslash }b$ to the left premise leads to contradiction with Lemma 9, exactly as in the proof of the previous lemma.