Non-associative Lambek Categorial Grammar in Polynomial Time

Erik Aarts^{1}

Research Institute for Dep. of Mathematics
Language and Speech and Computer Science
Utrecht University  University of Amsterdam
Trans 10  Plantage Muidergracht 24
3512 JK Utrecht  1018 TV Amsterdam

Kees Trautwein

Research Institute for Language and Speech Utrecht University Trans 10 3512 JK Utrecht

Abstract

We present a new axiomatization of the non-associative Lambek categorial grammar. We prove that it takes polynomial time to translate any nonassociative Lambek categorial grammar into an equivalent context-free grammar. Since it is possible to recognize a sentence generated by a context-free grammar in polynomial time, this proves that a sentence generated by any nonassociative Lambek categorial grammar can be recognized in polynomial time.

1 Introduction

In this paper we present an algorithm for the recognition of sentences generated by non-associative Lambek categorial grammars (see Lambek (1958) for details on the Lambek categorial grammar). First we will define categorial grammars. These grammars consist of a lexicon defining a type assignment to words, and a calculus defining the well-formed sequences of types. An important categorial grammar is the Lambek grammar which uses the Lambek calculus to define well-formedness. The complexity of the recognition problem for Lambek categorial grammar is still unknown. So far only nondeterministic polynomial time algorithms are known. On the other hand there isn’t any proof that this recognition problem is NP-complete.

For the second order fragment polynomial algorithms have been found (Aarts, 1993; Aarts, to appear). Another interesting fragment of the Lambek calculus is the non-associative calculus. The non-associative Lambek calculus can be obtained from the standard Lambek calculus by dropping the associativity rule. There are several ways to axiomatize the resulting calculus. Buszkowski (1986) proves that the nonassociative Lambek categorial grammar is equivalent with context-free grammar. The grammar that he obtains has exponential size. Only exponential time algorithms have been found in the past (Janssen, 1991; Trautwein, 1991). In this paper we present a new axiomatization of the non-associative Lambek calculus. This axiomatization enables us to give a polynomial translation into context-free grammars. After the translation we can use any context-free recognition algorithm to recognize a sentence generated by the non-associative Lambek categorial grammar in polynomial time.

1The author was sponsored by project NF 102/62-356 (’Structural and Semantic Parallels in Natural Languages and Programming Languages’), funded by the Netherlands Organization for the Advancement of Research (NWO).

2 Categorial Grammars

A categorial grammar G is defined by a lexicon Lex and a calculus C. A (finite) set of primitive types P r is given. T p is the set of types. Types are constructed from primitive types by two type-forming operators: / and \, i.e., T p is the smallest set including P r such that if x, y ∈ T p, then x\y, x/y ∈ T p. One member s of P r is singled out as the distinguished type.

A lexicon Lex is a finite relation between an alphabet Σ and T p (Lex ⊂ Σ × T p, Σ ∩ T p = ∅). If a lexicon Lex relates a ∈ Σ with A ∈ Tp (⟨a, A⟩ ∈ Lex), we say Lex assigns A to a.

ST p is the set of strings of types. Furthermore, we define the set BST p, of bracketed strings of types as the smallest set including T p such that if X, Y ∈ BST p, then (X, Y) ∈ BST p. The yield of a bracketed string X is the string we get when we erase the brackets. Yields are elements of ST p.

Now L(G) is defined to be the set of strings w ∈ Σ^{∗}, w = a_{1} … a_{n} such that for some bracketed string of types X, yield(X) = A_{1}, …, A_{n}, ⟨a_{i}, A_{i}⟩ ∈ Lex (1 ≤ i ≤ n) and X → s is derivable in the calculus C.

We use the non-associative Lambek calculus as the calculus C. There is a number of possible axiomatizations for this calculus. We choose one given in Kandulski (1988) as our starting point. This calculus is called NLG_{0} and can be found in Figure 1.

[A1] x → x , for x ∈ T p

\begin{matrix}{(X, y) → x \atop X → x/y} ^{[R1′]} & {(y, X) → x \atop X → y\x} ^{[R1′′]} \\ \begin{matrix}X → y & Y [x] → z \\ Y [(x/y, X)] → z \end{matrix} ^{[R2′]} & \begin{matrix}X → y & Y [x] → z \\ Y [(X, y\x)] → z \end{matrix} ^{[R2′′]} \end{matrix}

for X, Y ∈ BST p and x, y, z ∈ T p.

Figure 1: NLG_{0}

The notation Y [x] (resp. Y [X]) is used to indicate the bracketed string of types Y, in which, on a certain place, type x (resp. bracketed string of types X) occurs.

Before we show that sentences can be recognized in polynomial time we first introduce two auxiliary calculi: NLG_{0}^{∗} and NLG_{0}^{∗∗}. The calculus NLG_{0}^{∗} differs from NLG_{0} in that the X’s in the R1′ and R1′′ rules are restricted: they must be in T p instead of in BST p. The calculus NLG_{0}^{∗∗} differs from NLG_{0}^{∗} in that the X’s in the R2′ and R2′′ rules must be in T p instead of in BST p.

The calculus NLG_{0}^{∗∗} can be written down as follows (compared to NLG_{0}, X has been replaced by w):

[A1] x → x , for x ∈ T p

\begin{matrix}{(w, y) → x \atop w → x/y} ^{[R1′]} & {(y, w) → x \atop w → y\x} ^{[R1′′]} \\ \begin{matrix}w → y & Y [x] → z \\ Y [(x/y, w)] → z \end{matrix} ^{[R2′]} & \begin{matrix}w → y & Y [x] → z \\ Y [(w, y\x)] → z \end{matrix} ^{[R2′′]} \end{matrix}

for Y ∈ BST p and w, x, y, z ∈ T p.
Figure 2: NLG_{0}^{∗∗}

In the sequel, we are going to prove that NLG_{0}, NLG_{0}^{∗} and NLG_{0}^{∗∗} are equivalent. We prove the following inclusions:

• NLG_{0} ⊆ NLG_{0}^{∗} (Theorem 2.1)

• NLG_{0}^{∗} ⊆ NLG_{0}^{∗∗} (Theorem 2.2)

• NLG_{0}^{∗∗} ⊆ NLG_{0} (Theorem 2.3)

Theorem 2.1 For all k, if some sequent Γ → A containing k slashes is derivable in NLG_{0}, then it is also derivable in NLG_{0}^{∗}.

Proof: We prove this theorem with strong induction on the number of slashes (/,\) in a sequent. The base case is k = 0. The sequent must be an axiom. No R1′ or R1′′ rules are used so Theorem 2.1 holds for k = 0. Now we assume the induction hypothesis:

IH(k): For all i < k, if some sequent Δ → B containing i slashes is derivable in NLG_{0}, then Δ → B is also derivable in NLG_{0}^{∗}.

We have to prove that if some sequent Θ → C containing k slashes is derivable in NLG_{0}, then it is also derivable in NLG_{0}^{∗}.

Assume Θ → C is derivable in NLG_{0}. Then there is a proof Π of Θ → C. We will show that Θ → C is also derivable in NLG_{0}^{∗}. We consider various possibilities for the last step in the proof of Π. We assume that proofs are constructed from top to bottom, i.e., from the axioms we try to reach the conclusion. The last step in a proof is the step that proves the final conclusion.

Case 1: Π is an axiom. Then it is derivable in NLG_{0}^{∗} too.

Case 2: The last step in Π is an R2 rule or an R1 rule with X ∈ T p. The proof is easy. The premises of the last step contain fewer slashes than Θ → C. The induction hypothesis tells that the premises are derivable in NLG_{0}^{∗}. Use the NLG_{0}^{∗} proofs of the premises and the last rule of Π to construct a proof of Θ → C in NLG_{0}^{∗}.

Case 3: The last step in Π is some R1 rule (e.g. R1′, the other case is symmetric) with X ∈ BST p, but X ∉ T p.

⋮ . ; (X, b) → a ; X → a/b ^{[R1′]}

The induction hypothesis tells that (X, b) → a is derivable in NLG_{0}^{∗}. Consider the proof in NLG_{0}^{∗} of (X, b) → a. The last step in this proof is not an R1 rule because (X, b) ∉ T p. If (X, b) → a has been derived with an R2 rule, then we have various possibilities.

\begin{matrix}{… \atop (X, b) → a} & [R2] \\ X → a/b \end{matrix}_{[R1′]}

The type b is not involved in the rule R2 (case 3a) or it is involved (case 3b).

Case 3a: If b is not involved, then R2 can be R2′ or R2′′. The proof is similar for both cases. In the first case, the proof is of the form:

\begin{matrix}\begin{matrix}⋮ . ; X′ → y & ⋮ . ; (Z[c], b) → a \\ (Z[(c/y, X′)], b) → a \end{matrix} & [R2′] \\ Z[(c/y, X′)] → a/b \end{matrix}_{[R1′]}

We can transform this proof into the following proof:

\begin{matrix}⋮ . ; X′ → y & ⋮ . ; (Z[c], b) → a ; Z[c] → a/b ^{[R1′]} \\ Z[(c/y, X′)] → a/b \end{matrix}_{[R2′]}

The sequents Z[c] → a/b and X′ → y have fewer slashes than Z[(c/y, X′)] → a/b. The induction hypothesis tells that the two smaller sequents are provable in NLG_{0}^{∗}. Therefore, Z[(c/y, X′)] → a/b is also provable in NLG_{0}^{∗}.

Case 3b: If b is involved in the R2 rule it must be the functor. X cannot be the functor because X ∉ T p. Type b is of the form d\c.

\begin{matrix}\begin{matrix}⋮ . ; X → d & ⋮ . ; c → a \\ (X, d\c) → a \end{matrix} & [R2′] \\ X → a/(d\c) \end{matrix}_{[R1′]}

The induction hypothesis says that X → d is derivable in NLG_{0}^{∗}. Consider the proof of X → d in NLG_{0}^{∗}. The last step in this proof must be an R2 step because X ∉ T p. The proof is of the following form:

\begin{matrix}\begin{matrix}\begin{matrix}⋮ . ; X′ → y & ⋮ . ; Z[e] → d \\ Z[(e/y, X′)] → d \end{matrix} ^{[R2′]} & ⋮ . ; c → a \\ (Z[(e/y, X′)], d\c) → a \end{matrix} & [R2′′] \\ Z[(e/y, X′)] → a/(d\c) \end{matrix}_{[R1′]}

We can transform this into:

\begin{matrix}⋮ . ; X′ → y & \begin{matrix}\begin{matrix}⋮ . ; Z[e] → d & ⋮ . ; c → a \\ (Z[e], d\c) → a \end{matrix} & [R2′′] \\ Z[e] → a/(d\c) \end{matrix}_{[R1′]} \\ Z[(e/y, X′)] → a/(d\c) \end{matrix}_{[R2′]}

The induction hypothesis says that X′ → y and Z[e] → a/(d\c) have proofs in NLG_{0}^{∗}. Therefore Z[(e/y, X′)] → a/(d\c) has a proof in NLG_{0}^{∗}. This completes the proof of Theorem 2.1. □

Theorem 2.2 For all k, if some sequent Γ → A containing k slashes is derivable in NLG_{0}^{∗}, then it is also derivable in NLG_{0}^{∗∗}.

Proof: Proof with strong induction on the number of slashes k. The base case k = 0 is trivial. Now we assume the induction hypothesis:

IH(k): For all i < k, if some sequent Δ → B containing i slashes is derivable in NLG_{0}^{∗}, then Δ → B is also derivable in NLG_{0}^{∗∗}.

We have to prove that if some sequent Θ → C containing k slashes is derivable in NLG_{0}^{∗}, then it is also derivable in NLG_{0}^{∗∗}.

Assume Θ → C is derivable in NLG_{0}^{∗}. Then there is a proof Π of Θ → C in NLG_{0}^{∗}. We will show that Θ → C is also derivable in NLG_{0}^{∗∗}. We consider various possibilities for the last step in the proof of Π.

Case 1: Π is an axiom. Then it is derivable in NLG_{0}^{∗∗} too.

Case 2: The last step in Π is an R1 rule or an R2 rule with X ∈ T p. The premises of the last step contain fewer slashes than Θ → C. The induction hypothesis tells that the premises are derivable in NLG_{0}^{∗∗}. Use the NLG_{0}^{∗∗} proofs of the premises and the last rule of Π to construct a proof of Θ → C in NLG_{0}^{∗∗}.

Case 3: The last step in the proof is an R2 rule with X ∈ BST p, but X ∉ T p.

\begin{matrix}⋮ . ; X → y & ⋮ . ; Y [x] → z \\ Y [(x/y, X)] → z \end{matrix} ^{[R2′]}

The induction hypothesis says that X → y has a proof in NLG_{0}^{∗∗}. The last rule applied in the proof of this sequent cannot be an R1 rule, because X ∉ T p. So the last rule in the proof of X → y is an R2 rule, say R2′ (the R2′′ case is similar). We have the following proof:

\begin{matrix}\begin{matrix}⋮ . ; W → v & ⋮ . ; Z[d] → y \\ Z[(d/v, W)] → y \end{matrix} ^{[R2′]} & ⋮ . ; Y [x] → z \\ Y [(x/y, Z[(d/v, W)])] → z \end{matrix} ^{[R2′]}

where W is in T p. We can transform it as follows:

\begin{matrix}⋮ . ; W → v & \begin{matrix}⋮ . ; Z[d] → y & ⋮ . ; Y [x] → z \\ Y [(x/y, Z[d])] → z \end{matrix} ^{[R2′]} \\ Y [(x/y, Z[(d/v, W)])] → z \end{matrix}_{[R2′]}

The sequents W → v and Y [(x/y, Z[d])] → z have proofs in NLG_{0}^{∗∗} (induction hypothesis) and therefore Y [(x/y, Z[(d/v, W)])] → z has a proof in NLG_{0}^{∗∗} too. End of proof of Theorem 2.2. □

Theorem 2.3 Anything derivable in NLG_{0}^{∗∗} is also derivable in NLG_{0}.

Proof: This is trivial, any proof in NLG_{0}^{∗∗} is also a proof in NLG_{0}. □

From Theorems 2.1, 2.2 and 2.3 we know that NLG_{0} = NLG_{0}^{∗} = NLG_{0}^{∗∗}. We introduce another calculus now, called A1–R2–R3–R4. This calculus is defined as follows:

[A1] x → x , for x ∈ T p

\begin{matrix}\begin{matrix}w → y & z → x \\ w → x/(y\z) \end{matrix} ^{[R3’]} & \begin{matrix}w → y & z → x \\ w → (z/y)\x \end{matrix} ^{[R3”]} \\ \begin{matrix}w → y & z → x \\ w/x → y/z \end{matrix} ^{[R4’]} & \begin{matrix}w → y & z → x \\ x\w → z\y \end{matrix} ^{[R4”]} \\ \begin{matrix}w → y & Y [x] → z \\ Y [(x/y, w)] → z \end{matrix} ^{[R2′]} & \begin{matrix}w → y & Y [x] → z \\ Y [(w, y\x)] → z \end{matrix} ^{[R2′′]} \end{matrix}

for Y ∈ BST p and w, x, y, z ∈ T p.

Figure 3: A1–R2–R3–R4

Theorem 2.4 A1–R2–R3–R4 = NLG_{0}^{∗∗}

Proof: Let us repeat the calculus NLG_{0}^{∗∗} here.

[A1] x → x , for x ∈ T p

\begin{matrix}{(w, y) → x \atop w → x/y} ^{[R1′]} & {(y, w) → x \atop w → y\x} ^{[R1′′]} \\ \begin{matrix}w → y & Y [x] → z \\ Y [(x/y, w)] → z \end{matrix} ^{[R2′]} & \begin{matrix}w → y & Y [x] → z \\ Y [(w, y\x)] → z \end{matrix} ^{[R2′′]} \end{matrix}

for Y ∈ BST p and w, x, y, z ∈ T p.
Figure 4: NLG_{0}^{∗∗}

The last step in the proof of the premise of an R1 rule must be an R2 rule. Therefore we can replace R1′ and R1′′ by the following rules:

\begin{matrix}w → y & z → x \\ w → x/(y\z) \end{matrix} ^{[R3’ = R2′′ + R1′]}  \begin{matrix}w → y & z → x \\ w → (z/y)\x \end{matrix} ^{[R3” = R2′ + R1′′]}

\begin{matrix}w → y & z → x \\ w/x → y/z \end{matrix} ^{[R4’ = R2′ + R1′]}  \begin{matrix}w → y & z → x \\ x\w → z\y \end{matrix} ^{[R4” = R2′′ + R1′′]}

This proves Theorem 2.4. □

Observe that the antecedent of the conclusion of an R2 rule is not in T p. On the other hand, the antecedents of the premises and the conclusions of R3 and R4 rules are in T p. Hence, a proof in A1–R2–R3–R4 of a sequent with an antecedent in T p contains R3 and R4 rules only.

3 Recognition for non-associative categorial grammar

We have come to a point now where we can remove the brackets from our calculi. We define the bracket-free calculus NLG_{1}. The rules of NLG_{1} are:

[A1] x → x , for x ∈ T p

\begin{matrix}\begin{matrix}w → y & z → x \\ w → x/(y\z) \end{matrix} ^{[R3’]} & \begin{matrix}w → y & z → x \\ w → (z/y)\x \end{matrix} ^{[R3”]} \\ \begin{matrix}w → y & z → x \\ w/x → y/z \end{matrix} ^{[R4’]} & \begin{matrix}w → y & z → x \\ x\w → z\y \end{matrix} ^{[R4”]} \end{matrix}

\begin{matrix}x → y & Δ, w, Δ′ → z \\ Δ, w/y, x, Δ′ → z \end{matrix} ^{[R5′]}  \begin{matrix}x → y & Δ, w, Δ′ → z \\ Δ, x, y\w, Δ′ → z \end{matrix} ^{[R5′′]}

for Δ, Δ′ ∈ ST p and w, x, y, z ∈ T p.

Figure 5: NLG_{1}

This calculus differs from A1–R2–R3–R4 because the brackets in the rules R2′ and R2′′ are erased. This results in two new rules R5′ and R5′′.

There is a one-to-one correspondence between proofs in A1–R2–R3–R4 and NLG_{1}. We can prove the following lemma’s:

Lemma 3.1 If a bracketed sequent X → z is derivable in A1–R2–R3–R4, then yield(X) → z is derivable in NLG_{1}.

Proof: A proof in A1–R2–R3–R4 has the following shape:

\begin{aligned}{⋮ . R3-R4 \atop x_{1} → w_{1}} & \begin{matrix}{⋮ . R3-R4 \atop x_{2} → w_{2}} & \begin{matrix}{⋮ . R3-R4 \atop x_{3} → w_{3}} & ⋮ . ; Y_{3} → z \\ Y_{2} → z \end{matrix} ^{[R2]} \\ Y_{1} → z \end{matrix}_{[R2]} \\ & Y_{0} → z \end{aligned}_{[R2]}

The Y_{i} → z premises are the only premises containing brackets. When we leave out those brackets, we immediately obtain an NLG_{1} proof. □

Lemma 3.2 If a sequent Y → z is derivable in NLG_{1}, then there is an X such that yield(X) = Y and X → z is derivable in A1–R2–R3–R4.

Proof: If we have an NLG_{1} proof it has the following shape:

\begin{aligned}{⋮ . R3-R4 \atop x_{1} → w_{1}} & \begin{matrix}{⋮ . R3-R4 \atop x_{2} → w_{2}} & \begin{matrix}{⋮ . R3-R4 \atop x_{3} → w_{3}} & ⋮ . ; Y_{3} → z \\ Y_{2} → z \end{matrix} ^{[R5]} \\ Y_{1} → z \end{matrix}_{[R5]} \\ & Y_{0} → z \end{aligned}_{[R5]}

It is easy to add brackets to the Y_{i} such that we obtain an A1–R2–R3–R4 proof. □

Lemma’s 3.1 and 3.2 enable us to remove the brackets in the definition of grammaticality as well.

L(G) has been defined as the set of strings w ∈ Σ^{∗}, w = a_{1} … a_{n} such that for some bracketed string of types X, yield(X) = A_{1}, …, A_{n}, ⟨a_{i}, A_{i}⟩ ∈ Lex (1 ≤ i ≤ n) and X → s is derivable in NLG_{0}.

But the language can be defined bracket-free now: L′(G) is the set of strings w ∈ Σ^{∗}, w = a_{1} … a_{n} such that for some string of types A_{1}, …, A_{n}, ⟨a_{i}, A_{i}⟩ ∈ Lex (1 ≤ i ≤ n) and A_{1}, …, A_{n} → s in NLG_{1}.

Lemma 3.3 For every lexicon G, L′(G) = L(G).

Proof: Follows from Lemma’s 3.1 and 3.2, Theorem 2.4 and the fact that NLG_{0} = NLG_{0}^{∗∗}. □

Lemma 3.4 For all x, y ∈ T p, we can check in time O((|x| + |y|)^{2}) whether x → y is provable in NLG_{1}.

Proof: The antecedents of the premises and of the conclusions of the R3 and R4 rules have length one. The antecedent of the conclusion of an R5 rule has length bigger than one. Therefore, the proof of x → y consists of R3 and R4 rules only. The subformula property holds for the “R3–R4 calculus”. Let n be the number of slashes in x plus the number of slashes in y. n is linear in |x| + |y|. We have to compute at most O(n^{2}) times whether some a → b is derivable (because a and b are subformulas of x and y). We memoize (Cormen et al., 1990, pp. 312–314) the results of the attempts to prove something: the first time we have to compute a → b the result of the computation is stored in a table. If we have to compute it again later we look up the answer in the table. The search space is a graph with nodes labeled x → y. As said, there are O(n^{2}) nodes. Every node has at most four outgoing arcs: at most two rules of R3–R4 are applicable, so we have to prove at most 4 premises. Therefore, the number of arcs is O(4n^{2}) = O(n^{2}). The algorithm is a depth first traversal of the graph. Because of memoization, every arc is traversed only once. The algorithm takes time O(n^{2}) at most. □

Theorem 3.5 The recognition problem for non-associative Lambek categorial grammar can be reduced to context-free grammar recognition in polynomial time.

Proof: We take the new definition of categorial languages: L′(G) is the set of strings w ∈ Σ^{∗}, w = a_{1} … a_{n} such that for some string of types A_{1}, …, A_{n}, ⟨a_{i}, A_{i}⟩ ∈ Lex (1 ≤ i ≤ n) and A_{1}, …, A_{n} → s in NLG_{1}. The symbol s is the distinguished type of the grammar (s ∈ P r). Proofs in NLG_{1} look like:

\begin{aligned}{⋮ . R3-R4 \atop x_{1} → w_{1}} & \begin{matrix}{⋮ . R3-R4 \atop x_{2} → w_{2}} & \begin{matrix}{⋮ . R3-R4 \atop x_{3} → w_{3}} & ^{x_{n} → w_{n} s → s} _{[R5]} ; ⋮ . ; Y_{3} → s \\ Y_{2} → s \end{matrix}_{[R5]} \\ Y_{1} → s \end{matrix}_{[R5]} \\ & Y_{0} → s \end{aligned}_{[R5]}

The sequence s, …, Y_{3}, Y_{2}, Y_{1}, Y_{0} can be seen as a derivation in a context-free grammar. Given a lexicon, we construct a context-free grammar that generates the same language as the categorial grammar. The context-free grammar consists of binary and unary grammar rules. The start symbol is s. The binary rules simulate rewriting the symbols s, …, Y_{3}, Y_{2}, Y_{1}, Y_{0}. The unary rules simulate the lexical type assignment.

The binary rules are of the form w ⇒ w/y, x and w ⇒ x, y\w. Let the variables x, w/y, and y\w range over all possible subtypes in the lexicon. The rule w ⇒ w/y, x (or w ⇒ x, y\w) is added to the grammar when the sequent x → y is derivable in NLG_{1}. The unary rules (for lexical type assignment) are of the form A ⇒ a with ⟨a, A⟩ ∈ Lex.

The number of subtypes in the lexicon is linear in the size of the lexicon. The number of binary rules is kwadratic in the number of subtypes. Therefore, the size of the grammar is kwadratic in the size of the lexicon. Construction of the grammar takes polynomial time because we can compute x → y in polynomial time. □

The time complexity of context-free grammar recognition is O(|G|n^{3}) where |G| is the size of the grammar and n the length of the input sentence (Sippu and Soisalon-Soininen, 1988, p. 147). Via construction of the context-free grammar, we have a polynomial time algorithm for recognition in the non-associative Lambek categorial grammar. After construction of the grammar, the time complexity of recognition is cubic in the length of the string and kwadratic in the size of the lexicon.

A polynomial time algorithm for deciding provability in NLG_{1} can be given too. Because we do not have a lexicon anymore, the number of possible types is infinite. We cannot use a context-free grammar in the style described here because it would have infinitely many rules. But instead of computing the grammar in advance we can compute grammar rules “on the fly”. We try to combine adjacent types according to the schemes w ⇒ w/y, x and w ⇒ x, y\w and compute whether x → y is derivable in R3–R4.

Acknowledgements

We want to thank Kees Vermeulen for proofreading an earlier version of this paper.

References

Erik Aarts. Parsing second order Lambek grammar in polynomial time. In Paul Dekker and Martin Stokhof, editors, Proceedings of the Ninth Amsterdam Colloquium, pages 35–45. Institute for Logic, Language and Computation, University of Amsterdam, December 1993.

Erik Aarts. Proving theorems of the second order Lambek calculus in polynomial time. Studia Logica, to appear.

Wojciech Buszkowski. Generative capacity of the nonassociative Lambek calculus. Bull. Pol. Acad. Scie. Math., 34:507–516, 1986.

Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to algorithms. MIT Press, 1990.

Theo M.V. Janssen. On Properties of the Zielonka-Lambek Calculus. In Paul Dekker and Martin Stokhof, editors, Proceedings of the Eighth Amsterdam Colloquium, pages 303–308. Institute for Logic, Language and Computation, University of Amsterdam, December 1991.

Maciej Kandulski. The non-associative Lambek calculus. In W. Buszkowski, W. Marciszewski, and J. van Benthem, editors, Categorial Grammar, Linguistic and Literary Studies in Eastern Europe (LLSEE), pages 141–151. John Benjamins Publishing Company, Amsterdam–Philadelphia, 1988.

Joachim Lambek. The mathematics of sentence structure. American Mathematical Monthly, pages 154–169, 1958.

Seppo Sippu and Eljas Soisalon-Soininen. Parsing Theory, Vol. 1: Languages and Parsing. EATCS Monographs on Theoretical Computer Science. Springer Verlag, 1988.

Kees Trautwein. Een parseeralgoritme voor de niet associatieve Lambek calculus [a parsing algorithm for the non-associative lambek calculus]. Master’s thesis, University of Amsterdam, August 1991.