\section{Introduction}

The Lambek calculus~\cite{Lambek58} was introduced for describing natural language syntax
by means of type-logical (categorial) grammars. Further research on type-logical grammar
showed that the original system proposed by Lambek appears to be insufficient to cover
intrinsic linguistic phenomena, and so various extensions and modifications of the Lambek
calculus were introduced (see, for example, books by Morrill~\cite{MorrillBook},
Moot and Retor\'{e} \cite{MootRetore} and others). One of
these extensions is the {\em Lambek calculus with brackets} introduced by Moortgat~\cite{Moortgat}.
While the original Lambek calculus is fully associative, brackets block associativity in
specified situations, thus disallowing derivations of ungrammatical phrases like
``the girl whom John loves Mary and Pete loves'' (see~\cite{MorrillBook} for a more detailed
analysis).

The original Lambek grammars generate precisely context-free languages, as shown by Pentus~\cite{PentusCFG}.
For the Lambek calculus extended with brackets, the context-free upper bound was claimed by J\"ager~\cite{Jaeger}.
Unfortunately, J\"ager's argument relied upon a lemma by Versmissen~\cite{Versmissen}, which was
afterwards shown to be incorrect~\cite{FaddaMorrill}\cite{FSCD}. 

Recently, however, Kanazawa~\cite{KanazawaArXiv}
returned to this question and presented a new proof, based on a insightful combination of J\"ager's ideas and
the original Pentus' approach. Kanazawa proved this result for two versions of the Lambek calculus with brackets:
not allowing empty antecedents (we denote it by $\mathbf{Lb}$) and allowing them ($\mathbf{Lb}^{\boldsymbol{*}}$).

The third variant of the calculus, $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$, is obtained from $\mathbf{Lb}^{\boldsymbol{*}}$ by adding the {\em multiplicative unit constant,}
$\mathbf{1}$. As noticed by Kanazawa~\cite{KanazawaArXiv}, Pentus-style reasoning is not applicable to the case with
the unit constant (even without brackets). In Pentus' proof, the target context-free grammar rules are essentially
all derivable sequents of a bounded size. For $\mathbf{Lb}$ and $\mathbf{Lb}^{\boldsymbol{*}}$, the set of these sequents is finite; however,
the measure of size used by Pentus ignores occurrences of $\mathbf{1}$, thus this set of sequents becomes infinite, and
doesn't yield a context-free grammar. A workaround for this issue (in the case without brackets) was presented
by Kuznetsov~\cite{FG2011}: the unit constant gets eliminated by a faithful translation of the calculus with
the unit into the original system. The same problem for the case with brackets ({\it i.e.,} whether $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-grammars
generate precisely context-free languages) was left as an open question in~\cite{KanazawaArXiv}.

In this paper, we extend the construction from~\cite{FG2011} to an embedding of $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ into $\mathbf{Lb}^{\boldsymbol{*}}$.
Thus, we show that $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-grammars generate the same class of languages as $\mathbf{Lb}^{\boldsymbol{*}}$-grammars---and, due
to Kanazawa~\cite{KanazawaArXiv}, it is the class of context-free languages.

The translation of $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ to $\mathbf{Lb}^{\boldsymbol{*}}$ also has an algorithmic application. While the original Lambek calculus,
and, therefore, the Lambek calculus with brackets is NP-complete (Pentus~\cite{PentusNP}), for sequents of
bounded formula complexity and bracket nesting depth Kanovich {\it et al.}~\cite{FSCD}, extending Pentus~\cite{PentusPoly},
present a polynomial-time algorithm for deciding derivability in $\mathbf{Lb}^{\boldsymbol{*}}$. Our translation generalises this algorithm
from $\mathbf{Lb}^{\boldsymbol{*}}$ to $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$.



\section{The Calculi $\mathbf{Lb}^{\boldsymbol{*}}$ and $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$}

In this section and further we use the notation of~\cite{FSCD}; the notation used 
in~\cite{KanazawaArXiv} is slightly different.


The syntax of the Lambek calculus with brackets is a bit more involved than a standard
sequential calculus. Formulae of $\mathbf{Lb}^{\boldsymbol{*}}$ are recursively built from variables
($\mathrm{Var} = \{ p_1, p_2, \dots \}$) using three binary connectives,
$\mathop{\backslash}$ (left division), $\mathop{/}$ (right division), $\cdot$ (product) and two unary ones,
$\langle\rangle$ and $[]^{-1}$. The binary connectives come from the original Lambek calculus~\cite{Lambek58};
as one can easily see, the system $\mathbf{Lb}^{\boldsymbol{*}}$ defined below is a conservative extension of the
version of the Lambek calculus which allows empty antecedents~\cite{Lambek61}. The unary
connectives operate brackets that are used to introduce controlled non-associativity.
Sequents of $\mathbf{Lb}^{\boldsymbol{*}}$ are expressions of the form $\Pi \to C$, where $C$ is a formula and
$\Pi$ is a {\em meta-formula.} Meta-formulae are built from formulae using comma (,) and
brackets ([...]). By definition, comma is associative, and the empty meta-formula $\Lambda$
is the unit object w.r.t.\ comma: $\Gamma,\Lambda$ and $\Lambda,\Gamma$ are both considered
graphically equal to $\Gamma$. By $\Delta(\Pi)$ we denote a meta-formula $\Delta$ with
a {\em designated occurrence} of a sub-meta-formula $\Pi$.

Axioms and rules of $\mathbf{Lb}^{\boldsymbol{*}}$ are as follows.


$$
\infer[(\mathrm{ax})]{p_i \to p_i}{}
$$
$$
\infer[(\mathop{\backslash}\to)]{\Delta(\Pi, A \mathop{\backslash} B) \to C}{\Pi \to A & \Delta(B) \to C}
\qquad
\infer[(\to\mathop{\backslash})]{\Pi \to A \mathop{\backslash} B}{A, \Pi \to B}
$$
$$
\infer[(\mathop{/}\to)]{\Delta(B \mathop{/} A, \Pi) \to C}{\Pi \to A & \Delta(B) \to C}
\qquad
\infer[(\to\mathop{/})]{\Pi \to B \mathop{/} A}{\Pi, A \to B}
$$
$$
\infer[(\cdot\to)]{\Delta(A \cdot B) \to C}{\Delta(A, B) \to C}
\qquad
\infer[(\to\cdot)]{\Pi, \Gamma \to A \cdot B}{\Pi \to A & \Gamma \to B}
$$
$$
\infer[(\langle\rangle\to)]{\Delta(\langle\rangle A) \to C}{\Delta([A]) \to C}
\qquad
\infer[(\to\langle\rangle)]{[\Pi] \to \langle\rangle A}{\Pi \to A}
$$
$$
\infer[([]^{-1}\to)]{\Delta([[]^{-1} A]) \to C}{\Delta(A) \to C}
\qquad
\infer[(\to[]^{-1})]{\Pi \to []^{-1} A}{[\Pi] \to A}
$$


Adding the unit constant, $\mathbf{1}$, with the following rules of inference (cf.~\cite{Lambek69}),
$$
\infer[(\mathbf{1}\to)]{\Delta(\mathbf{1}) \to C}{\Delta(\Lambda) \to C}
\qquad
\infer[(\to\mathbf{1})]{\to\mathbf{1}}{}
$$
yields the calculus $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$. 

The cut rule of the following form is admissible~\cite{Moortgat}.
$$
\infer[(\mathrm{cut})]{\Delta(\Pi) \to C}{\Pi \to A & \Delta(A) \to C}
$$
Admissibility of cut allows replacing a subformula with an equivalent one preserving
derivability. 

\section{Translating $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ to $\mathbf{Lb}^{\boldsymbol{*}}$}

In this section we present a translation of $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ formulae that eliminates the unit constant.

Informally, we replace each occurrence of $\mathbf{1}$ by $(q \mathop{\backslash} q)$, where
$q$ is a fresh variable. For classical propositional logic, this would be sufficient, since
$(\varphi \Rightarrow \varphi)$ there is equivalent to the ``{\sc true}'' constant. In order to make
this construction work for the substructural
system $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$, however, we also need to add some extra $(q \mathop{\backslash} q)$'s,
depending on the polarity of specific subformula.

Formally, we define two translations, $\tau^+$ and $\tau^-$, by joint induction:
\begin{align*}
& \tau^+(\mathbf{1}) = \tau^-(\mathbf{1}) = q \mathop{\backslash} q\\
& \tau^+(p_i) = (q \mathop{\backslash} q) \cdot p_i \cdot (q \mathop{\backslash} q) && \tau^-(p_i) = p_i\\
& \tau^+(A \mathop{\backslash} B) = \tau^-(A) \mathop{\backslash} \tau^+(B) && \tau^-(A \mathop{\backslash} B) = \tau^-(A) \mathop{\backslash} \tau^-(B) \\
& \tau^+(B \mathop{/} A) = \tau^+(B) \mathop{/} \tau^+(A) && \tau^-(B \mathop{/} A) = \tau^-(B) \mathop{/} \tau^+(A)\\
& \tau^+(A \cdot B) = \tau^+(A) \cdot \tau^+(B) && \tau^-(A \cdot B) = \tau^-(A) \cdot \tau^-(B)\\
& \tau^+(\langle\rangle A) = (q \mathop{\backslash} q) \cdot \langle\rangle \tau^+(A) \cdot (q \mathop{\backslash} q) &&
\tau^-(\langle\rangle A) = \langle\rangle \tau^-(A)\\
& \tau^+([]^{-1} A) = []^{-1} \tau^-(A) && 
\tau^-([]^{-1} A) = (q \mathop{\backslash} q) \mathop{\backslash} []^{-1} \tau^-(A) \mathop{/} (q \mathop{\backslash} q)
\end{align*}

For metaformulae, we define only $\tau^-$:
\begin{align*}
&\tau^-(\Lambda) = \Lambda\\
&\tau^-(\Gamma, \Delta) = \tau^-(\Gamma), \tau^-(\Delta)\\
&\tau^-([\Gamma]) = [\tau^-(\Gamma)]
\end{align*}



\begin{theorem}\label{Th:main}
For any $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-sequent $\Pi \to C$ that has no occurrences of $q$,
$\Pi \to C$ is derivable in $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ if{f} $\tau^-(\Pi) \to \tau^+(B)$ is
derivable in $\mathbf{Lb}^{\boldsymbol{*}}$.
\end{theorem}

In order to make the proof more convenient, we first reformulate $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$: remove $(\mathbf{1}\to)$ and replace some of the other rules with the following ones
(here and further $\mathbf{1}^n$ means $\underbrace{\mathbf{1}, \mathbf{1}, \dots, \mathbf{1}}_{\text{$n$ times}}$).
$$
\infer[(\to\mathbf{1})']
{\mathbf{1}^k \to \mathbf{1}}{}
\qquad
\infer[(\mathrm{ax})']
{\mathbf{1}^k, p_i, \mathbf{1}^m \to p_i}{}
$$
$$
\infer[(\to\langle\rangle)']
{\mathbf{1}^k, [\Pi], \mathbf{1}^m \to \langle\rangle A}
{\Pi \to \langle\rangle A}
\qquad
\infer[([]^{-1}\to)']
{\Delta([\mathbf{1}^k, []^{-1} B, \mathbf{1}^m]) \to C}
{\Delta(B) \to C}
$$
All other rules are left intact.

Let's call the new calculus ${\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}}'$.

\begin{lemma}\label{Lm:LbUp}
A sequent is derivable in ${\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}}'$ if{f} it is derivable in 
$\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$.
\end{lemma}

\begin{proof}
Since the new $'$-rules become the original rules of $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ when $k=m=0$, for the
``if'' part it is sufficient to show that $(\mathbf{1}\to)$ is admissible in ${\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}}'$, {\em i.e.,}
that if $\Psi(\Lambda) \to C$ is derivable in ${\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}}'$, then so is $\Psi(\mathbf{1}) \to C$.


Proceed by induction on derivation.
Let's denote $\Pi$, $\Gamma$, and $\Delta$ (except for the designated part that is affected by the rule) 
in the rules of $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ as the {\em context}. Consider the last rule that derives $\Psi(\Lambda) \to C$.

If this designated occurrence of $\Lambda$ is inside the context of the last rule that derives $\Psi(\Lambda) \to C$,
then we can trace it upwards to the premise (one of the premises) of the rule, replace $\Lambda$ by $\mathbf{1}$ there
(the sequent is still derivable by induction hypothesis), and then apply the rule. In other words, in this case
the two rules are exchangeable, and we can propagate the $(\mathbf{1}\to)$ rule upwards. For $(\mathop{/}\to)$, $(\mathop{\backslash}\to)$,
$(\to\mathop{/})$, $(\to\mathop{\backslash})$, $(\cdot\to)$, $(\to\cdot)$, $(\langle\rangle\to)$, and $(\to[]^{-1})$ this is the only possible
situation: a possible place for inserting $\mathbf{1}$ is always in the context.

If $\Psi(\Lambda) \to C$ is an axiom of the form $(\mathrm{ax})'$, namely, $\mathbf{1}^k, p_i, \mathbf{1}^m \to p_i$, then $\Psi(\mathbf{1}) \to C$ is either 
$\mathbf{1}^{k+1}, p_i, \mathbf{1}^m \to p_i$ or $\mathbf{1}^k, p_i, \mathbf{1}^{m+1} \to p_i$; both are again instances of $(\mathrm{ax})'$. The $(\to\mathbf{1})'$ case
is handled in the same way. For the $(\to\langle\rangle)'$ case, the only interesting situation is when $\mathbf{1}$ is added outside
the brackets (the case when it is added into the context $\Pi$, was already considered); in this situation the extra $\mathbf{1}$ again
gets absorbed by the $(\to\langle\rangle)'$ rule. The $([]^{-1}\to)'$ case is dual.


For the ``only if'' part, just notice that each $'$-rule can be represented as a
consequent application of the corresponding rule of $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ and then $k+m$ times
$(\mathbf{1}\to)$  (or $k$ times for $(\to\mathbf{1})'$). 
\end{proof}

\begin{proof}[Proof of Theorem~\ref{Th:main}]
The ``only if'' part: let $\Pi \to C$ be derivable in $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$. Then by Lemma~\ref{Lm:LbUp}
it is derivable in ${\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}}'$. We need to show that $\tau^-(\Pi) \to \tau^+(C)$ is derivable
in $\mathbf{Lb}^{\boldsymbol{*}}$. Proceed by induction on the derivation of $\Pi\to C$ in ${\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}}'$. Applications of rules
without $'$ are translated into $\mathbf{Lb}^{\boldsymbol{*}}$ ``as is.'' The $(\to\mathbf{1})'$ transforms into $(q\mathop{\backslash} q)^k \to q \mathop{\backslash} q$,
which is derivable in $\mathbf{Lb}^{\boldsymbol{*}}$; $(\mathrm{ax})'$ becomes $(q \mathop{\backslash} q)^k, p_i, (q \mathop{\backslash} q)^m \to (q \mathop{\backslash} q) \cdot p_i \cdot (q \mathop{\backslash} q)$,
which is also derivable. Finally, $(\to\langle\rangle)'$ and $([]^{-1}\to)'$ are translated as follows:
$$
\infer[(\to\cdot) \text{ two times}]{(q \mathop{\backslash} q)^k, [\tau^-(\Pi)], (q \mathop{\backslash} q)^m \to (q \mathop{\backslash} q) \cdot \langle\rangle \tau^+(A) \cdot (q \mathop{\backslash} q)}
{(q \mathop{\backslash} q)^k \to q \mathop{\backslash} q & \infer[(\to\langle\rangle)]{[\tau^-(\Pi)] \to \langle\rangle \tau^+(A)}{\tau^-(\Pi) \to \tau^+(A)} & (q \mathop{\backslash} q)^m \to q \mathop{\backslash} q}
$$
$$
\infer[(\mathop{\backslash}\to) \text{ and } (\mathop{/}\to)]
{\Delta([(q \mathop{\backslash} q)^k, (q \mathop{\backslash} q) \mathop{\backslash} []^{-1} \tau^-(B) \mathop{/} (q \mathop{\backslash} q), (q \mathop{\backslash} q)^m]) \to C}
{(q \mathop{\backslash} q)^k \to q \mathop{\backslash} q & \infer[([]^{-1}\to)]{\Delta([[]^{-1} \tau^-(B)]) \to C}{\Delta(\tau^-(B)) \to C} &
(q \mathop{\backslash} q)^m \to q \mathop{\backslash} q}
$$

The ``if'' part is easier: if $\tau^-(\Pi) \to \tau^+(C)$ is derivable in $\mathbf{Lb}^{\boldsymbol{*}}$, then it is also derivable in $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$.
Substitute $\mathbf{1}$ for $q$ (substituting formulae for variables---but not for the unit constant!---preserves derivability).
Since $q$ is a fresh variable, the substitution affects only the $(q \mathop{\backslash} q)$ combinations introduced by $\tau^+$ and $\tau^-$,
and it is easy to see that for any formula $B$ after this substitution $\tau^+(B)$ and $\tau^-(B)$ become equivalent to $B$.
Thus, $\tau^-(\Pi) \to \tau^+(C)$ transforms to a sequent equivalent to $\Pi \to C$, therefore the latter one is derivable in $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$.
\end{proof}

\section{Applications}

The first application of Theorem~\ref{Th:main} is the characterisation of the class of languages generated by
$\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-grammars. 

Let $\Sigma$ be a finite alphabet. An $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-grammar over $\Sigma$ is a triple $\langle \rhd, H \rangle$, where
$H$ is an $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-formula (called the {\em target} formula), and $\rhd$ is a finite relation between letters $\Sigma$ and 
$\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-formulae. J\"ager~\cite{Jaeger} gives two definitions of a word $a_1\dots a_n$ being accepted by such a grammar.
The word is {\em s-accepted,} if there exist such formulae $A_1, \dots, A_n$ that $a_i \rhd A_i$ ($i = 1,\dots, n)$ and
the sequent $A_1, \dots, A_n \to H$ is derivable in $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$. The word is {\em t-accepted,} if, again, there exist $A_1, \dots, A_n$
such that $a_i \rhd A_i$, and there also exists a multiformula $\Pi$ such that $\Pi \to H$ is derivable and $A_1, \dots, A_n$
is obtained from $\Pi$ by erasing $[$ and $]$ ({\it i.e.,} it is the {\em yield} of the treelike bracketed structure $\Pi$).
The language t-generated (resp., s-generated) by the grammars defined as the set of all t-accepted (resp., s-accepted) words.

Theorem~\ref{Th:main} immediately yields the following corollary:
\begin{theorem}
The class of languages t-generated (resp., s-generated) by $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-grammars, coincides with the class of languages
t-generated (resp., s-generated) by $\mathbf{Lb}^{\boldsymbol{*}}$-grammars.
\end{theorem}

\begin{proof}
For the inclusion in the non-trivial direction, apply $\tau^-$ to all formulae associated to letters of
$\Sigma$ by $\rhd$, and $\tau^+$ to the target formula $H$.
\end{proof}

In combination with Kanazawa's result that $\mathbf{Lb}^{\boldsymbol{*}}$-grammars t-generate exactly the class of context-free languages,
this gives a solution for the question left open in~\cite{KanazawaArXiv}: $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$-grammars also t-generate exactly all
context-free languages. We conjecture that our construction also works for the multimodal version of $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$, 
solving the second open question from~\cite{KanazawaArXiv}.
The question about the class of s-generated languages appears to be still open, though much less interesting from
the linguistic point of view.

The second application is a fast algorithm for deciding derivability in $\mathbf{Lb}^{\boldsymbol{*}}$. While the full Lambek calculus is
NP-complete~\cite{PentusNP}, Pentus in~\cite{PentusPoly} introduces a depth parameter $d$ (in the product-free
case it is just the Horn depth of $\mathop{\backslash}$ and $\mathop{/}$) and presents an algorithm that works in polynomial time w.r.t.\ $n$
and $2^d$ (where $n$ is the length of the input sequent). Kanovich {\em et al.}~\cite{FSCD} generalise this
algorithm to $\mathbf{Lb}^{\boldsymbol{*}}$, adding the third parameter, $b$, which is the nesting depth of $[...]$, $\langle\rangle$, and $[]^{-1}$. The running
time of this algorithm is bounded by a polynom of $n$, $2^d$, and $n^b$ (if there are brackets, $n^b$ absorbs $n$). Since $\tau^+$ and
$\tau^-$ alter these parameters only linearly, Theorem~\ref{Th:main} yields an algorithm also for $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ with the same running
time estimation:
\begin{theorem}
There exists an algorithm that decides derivability in $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$ with running time bounded by a polynom of
$n$, $2^d$, and $n^b$.
\end{theorem}

\subsection*{Acknowledgments}

The author
was much inspired by recent and older works of Makoto Kanazawa (to which this note is a modest addition).
The author is also grateful to Lev Beklemishev, Max Kanovich, Glyn Morrill, Vivek Nigam, Mati Pentus, and Andre Scedrov for 
in-depth discussions and exchange of ideas in a very warm, friendly, and collaborative atmosphere. 


