We prove that the Lambek calculus is complete w.r.t. L-models, i.e., free semigroup models. We also prove the completeness w.r.t. relativized relational models over the natural linear order of integers.

In this paper we prove the Chomsky Conjecture (all languages recognized by the Lambek calculus are context-free) for both the full Lambek calculus and its product-free fragment. For the latter case we present a construction of context-free grammars involving only product-free types.

In 1958 J. Lambek introduced a calculusL of syntactic types and defined an equivalence relation on types: x y means that there exists a sequence x=x1,...,xn=y (n 1), such thatx i x i+1 or xi+ x i (1 i n). He pointed out thatx y if and only if there is joinz such thatx z andy z. This paper gives an effective characterization of this equivalence for the Lambeck calculiL andLP, and for the multiplicative fragments of Girard's and Yetter's linear (...) logics. Moreover, for the non-directed Lambek calculusLP and the multiplicative fragment of Girard's linear logic, we present linear time algorithms deciding whether two types are equal, and finding a join for them if they are. (shrink)