Lambek grammars with one division and one primitive type
S. Kuznetsov · Logic Journal of IGPL · 2011
We prove that a formal language without the empty word is context-free if and only if it is generated by some L(∖; p1)-grammar, where L(∖; p1) is the Lambek calculus with one division and one primitive type. To do that, we use a substitution of types which reduces derivability in L(∖) to derivability in L(∖; p1). We also prove that a formal language (possibly, with the empty word) is context-free if and only if it is generated by some L*(∖; p1)-grammar (where L*(∖; p1) is a variant of L(∖; p1) that allows empty premises). To do that, we introduce a construction which adds the empty word to languages generated by a special subclass of L*(∖)-grammars (which covers all context-free languages without the empty word) and then use the same substitution as for L(∖).