Non-commutative linear logic fragments with sub-context-free complexity

TL;DR

This paper characterizes the complexity of certain non-commutative linear logic fragments, linking them to formal language classes and demonstrating their computational properties through novel proof-theoretic methods.

Contribution

It provides the first proof complexity characterizations of Lambek calculus fragments corresponding to regular and linear context-free languages, using a new translation and structural induction approach.

Findings

Lambek calculus fragments correspond to REG and LCFL complexity classes.

A single-inference rule variant of the logic is shown to be CFL-complete.

The proof employs a direct translation between type-logical and formal grammar.

Abstract

We present new descriptive complexity characterisations of classes REG (regular languages), LCFL (linear context-free languages) and CFL (context-free languages) as restrictions on inference rules, size of formulae and permitted connectives in the Lambek calculus; fragments of the intuitionistic non-commutative linear logic with direction-sensitive implication connectives. Our identification of the Lambek calculus fragments with proof complexity REG and LCFL is the first result of its kind. We further show the CFL complexity of one of the strictly `weakest' possible variants of the logic, admitting only a single inference rule. The proof thereof, moreover, is based on a direct translation between type-logical and formal grammar and structural induction on provable sequents; a simpler and more intuitive method than those employed in prior works. We thereby establish a clear conceptual utility of the Cut-elimination theorem for comparing formal grammar and sequent calculus, and identify the exact analogue of the Greibach Normal Form in Lambek grammar. We believe the result presented herein constitutes a first step toward a more extensive and richer characterisation of the interaction between computation and logic, as well as a finer-grained complexity separation of various sequent calculi.