The Lambek Calculus with Iteration (Kleene Star)
Stepan Kuznetsov
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia
Besides multiplication (pairwise concatenation, A dot B) of formal languages, there are also two division operations on them: A dot B is included in C iff B is included in (A C) iff A is included in (C / B). The Lambek calculus was designed to describe all universally true statements of the form “A is included in B”, where A and B are formulas built using the three connectives (multiplication and two divisions). The completeness theorem was proved by Pentus (1995). It looks natural to consider also other well-known operations on formal languages, and one of these operations is the Kleene star, or iteration. Though this operation is very standard, the problem of enriching the Lambek calculus with this new unary connective in a proper way appears to be quite hard. We present two lines of calculi. The first one uses omega-rules or derivation trees with infinite branches, and we prove cut-elimination and completeness of the product-free fragment, but, as the derivations are infinite, we do not get any algorithmic properties, even recursive enumerability. The second approach is to formalize the Kleene star in an inductive manner. We present a Hilbert-style axiomatization and also a sequent calculus with cyclic derivations. This system is sound with respect to the intended interpretation. Completeness, or, in other words, whether the system with omega-rules is stronger than the inductive one, remains an open question.
Ph.D. of 2012 “Categorial Grammars Based on Variants of the Lambek Calculus” under Mati Pentus, Moscow University.