A Polynomial-Time Algorithm for Lambek Grammars of Bounded Order
We present a deterministic algorithm for solving the derivability problem for the Lambek calculus (the syntactic calculus with left division, right division, and multiplication, introduced by J. Lambek in 1958) and a similar algorithm for the Lambek calculus allowing empty premises. These algorithms work in time polynomial in the input length if the order of all syntactic types is bounded by a constant (it is known that for unbounded order the derivability problem is NP-complete). The algorithms are based on a method for deciding derivability in the multiplicative fragment of the cyclic linear logic. This method also yields an algorithm for solving the membership problem in Lambek grammars, which works in time polynomial in the grammar size and string length provided the order of all syntactic types is bounded by a constant.