2025-11-11T14:52:08.882681

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

Nishimiya, Taniguchi

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.

academic

部分交換非線形論理の部分文脈自由複雑性を持つ断片

基本情報

論文ID: 2511.02348
タイトル: Non-commutative linear logic fragments with sub-context-free complexity
著者: Yusaku Nishimiya (University of Illinois Springfield & RIKEN AIP)、Masaya Taniguchi (RIKEN AIP)
分類: cs.LO (計算機科学における論理)、cs.CC (計算複雑性)、cs.FL (形式言語)、math.LO (数学論理)
発表日時: 2025年11月4日 (arXivプレプリント)
論文リンク: https://arxiv.org/abs/2511.02348

要約

本論文は、正則言語(REG)、線形文脈自由言語(LCFL)、および文脈自由言語(CFL)の3つの言語クラスに対する新しい記述複雑性刻画を提案している。これはLambek計算における推論規則、公式サイズ、および許容される連結詞の制限を通じて実現される。Lambek計算は直観主義的非交換線形論理の断片であり、方向敏感な含意連結詞を備えている。著者らは初めてREGおよびLCFL証明複雑性を持つLambek計算の断片を特定し、単一の推論規則のみを許容する「最弱」論理変種のCFL複雑性を示した。証明は型論理文法と形式文法間の直接翻訳および証明可能な列の構造帰納法に基づいており、先行研究で採用された方法よりも単純で直感的である。

研究背景と動機

問題背景

部分構造論理の研究: 証明論研究者は部分構造論理を研究して、構造規則の許容または除去が証明システムの性質に与える影響を理解している。通常、シークエント計算の形式で提示される。
線形論理の計算的意義: 線形論理(LL)は収縮および弱化規則を制限し、証明を古典論理よりもリソース意識的にする。したがって計算とより関連性がある。MALLはPSPACE-completeであり、MLLはNP-completeであることが知られている。
Lambek計算の表現力: Lambek計算Lはllの直観主義的、非交換的、乗法的断片であり、方向敏感な含意を備えている。Pentusはlambek文法と文脈自由文法の等価性を証明したが、Chomsky階層構造内の下位言語クラスに対応するL断片はまだ特定されていない。

研究動機

既存研究はLL「より弱い」断片の計算複雑性についてほとんど理解していない。特に、正則言語および線形文脈自由言語に対応するLambek計算断片の刻画が不足している。本論文はこのギャップを埋め、論理公式のサイズと方向性制限と文法表現力の変化間の正確な対応関係を確立することを目指している。

核心的貢献

初めての特定: REGおよびLCFL証明複雑性を持つLambek計算断片を初めて特定した
最弱変種のCFL複雑性: 単一の推論規則のみを許容する論理変種がCFL複雑性を持つことを証明した
直接翻訳方法: 型論理文法と形式文法間の直接翻訳および構造帰納法を提供した
Cut除去定理の応用: Cut除去定理が形式文法とシークエント計算の比較における概念的有用性を確立した
Greibach標準形の類似: Lambek文法におけるGreibach標準形の正確な類似を特定した

方法の詳細説明

タスク定義

本論文は、Lambek計算の推論規則、公式サイズ、および連結詞を制限することにより、異なる複雑性クラスの形式言語をどのように刻画するかを研究している。具体的なタスクは、Lambek計算断片とChomsky階層構造内の言語クラス間の等価関係を確立することである。

理論的フレームワーク

Lambek計算の定義

Lambek計算Lは以下を含む：

公理: α → α
Cut規則: Γ,α,Θ → βおよびΔ → αからΓ,Δ,Θ → βを推出
6つの推論規則: 3つの二項連結詞/、\、および·に関する左右規則

主要概念

型度数d(α): 型αにおける連結詞の異なる出現数
型集合: Tp(/)は/連結詞のみを含む型集合を表し、Tpnは度数≤nの型集合を表す
Lambek文法: 四つ組(Pr, V, SG, f)。ここでfは型割り当て関数

核心定理

定理2 (主要結果): 以下の3つのLambek断片文法と形式文法のペアは等価な表現力を持つ：

L(/ →)-文法 with Tp(/) ⇔ CFG
L(/ →, \ →)-文法 with Tp1(/, ) ⇔ LCFG
L(/ →)-文法 with Tp1(/) ⇔ REG

証明戦略

可約性条件 (補題3)

Tp(/)内の空でない型列Γに対して、L(/ →) ⊢ Γ → SGが成立するのは以下の場合のみである：

Γ = α,Δ1,...,Δnであり、αは(···((S/βn)/βn-1)/···)/β1の形
すべての1≤k≤nに対して、L(/ →) ⊢ Δk → βk

構成方法

CFGからLambek文法へ: Greibach標準形を仮定し、生成規則A → aB1···Bnを型割り当て(···((A/Bn)/Bn-1)/···)/B1 ∈ f(a)に変換
Lambek文法からCFGへ: 型割り当て(···((α/βn)/βn-1)/···)/β1 ∈ f(a)を生成規則α → aβ1β2···βnに変換