Eliminating the unit constant in the Lambek calculus with brackets

TL;DR

This paper introduces a translation method that eliminates the unit constant from the Lambek calculus with brackets, extending known results about language generation and decision algorithms to this simplified calculus.

Contribution

It provides a translation from Lambek calculus with brackets and unit constant to a version without the unit, enabling the extension of key theoretical and computational results.

Findings

Languages generated are context-free

Decidability of derivability in polynomial time for bounded depth sequents

Extension of previous results to the calculus without the unit

Abstract

We present a translation of the Lambek calculus with brackets and the unit constant, $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$, into the Lambek calculus with brackets allowing empty antecedents, but without the unit constant, $\mathbf{Lb}^{\boldsymbol{*}}$. Using this translation, we extend previously known results for $\mathbf{Lb}^{\boldsymbol{*}}$ to $\mathbf{Lb}^{\boldsymbol{*}}_{\mathbf{1}}$: (1) languages generated by categorial grammars based on the Lambek calculus with brackets are context-free (Kanazawa 2017); (2) the polynomial-time algorithm for deciding derivability of bounded depth sequents (Kanovich et al. 2017).