2021/01/10 by Hiroyoshi Komatsu, Komatsu, Hiroyoshi
Computer Science · Mathematics · #Advanced Algebra and Logic #Computability, Logic, AI Algorithms #Computation and Language (cs.CL) #FOS: Computer and information sciences #Mathematical and Theoretical Analysis
paper · pdf · doi:10.48550/arxiv.2101.03634
openalex publication_date 2021/01/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.