The Logic for a Mildly Context-Sensitive Fragment of the Lambek-Grishin Calculus

TL;DR

This paper introduces HLG, a proof-theoretic logic that characterizes tree-adjoining languages within the Lambek-Grishin calculus, providing a formal framework for mildly context-sensitive languages.

Contribution

It presents HLG, a novel logic based on the Lambek-Grishin calculus, capturing tree-adjoining languages and extending the proof-theoretic understanding of mildly context-sensitive languages.

Findings

HLG is defined in display calculus with cut-admissibility.

New techniques like structural connectives and proof net graph-theoretic arguments are introduced.

HLG provides a formal proof-theoretic characterization of tree-adjoining languages.

Abstract

While context-free grammars are characterized by a simple proof-theoretic grammatical formalism namely categorial grammar and its logic the Lambek calculus, no such characterizations were known for tree-adjoining grammars, and even for any mildly context-sensitive languages classes in the last forty years despite some efforts. We settle this problem in this paper. On the basis of the existing fragment of the Lambek-Grishin calculus which captures tree-adjoining languages, we present a logic called HLG: a proof-theoretic characterization of tree-adjoining languages based on the Lambek-Grishin calculus restricted to Hyperedge-replacement grammar with rank two studied by Moot. HLG is defined in display calculus with cut-admissibility. Several new techniques are introduced for the proofs, such as purely structural connectives, usefulness, and a graph-theoretic argument on proof nets for HLG.