The Logic for a Mildly Context-Sensitive Fragment of the Lambek-Grishin Calculus
This work provides a foundational proof-theoretic characterization for Tree-Adjoining Grammars, which is significant for researchers in formal language theory and computational linguistics.
This paper addresses the long-standing problem of finding a proof-theoretic characterization for mildly context-sensitive languages, specifically Tree-Adjoining Grammars (TAGs). The authors introduce HLG, a logic based on the Lambek-Grishin calculus restricted to Hyperedge-replacement grammar with rank two, which provides such a characterization.
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.