【MLG60発表報告】ランベック計算に循環証明を導入する試み

2025-12-19

2025年12月19日、数理論理学の集会であるMLG60にて、「ランベック計算の循環証明体系 $L μ$ の試み」というタイトルで発表を行いました。本記事では、言語学的な動機を持つランベック計算に循環証明を導入する意義と、形式言語理論における含意について解説します。

背景と動機：論理と形式言語の階層構造

通常の Lambek Calculus ( $L$ ) は文脈自由文法 (CFG) と等価です。近年、論理側の制約（深さ制限など）を強めることで、正規言語や線形言語に対応する階層構造が整理されつつあります。本研究の目的は、この図式に「循環（サイクル）」、すなわち無限の証明構造を導入した $μ$ -Lambek calculus ( $L μ$ ) を加えることで、この階層がどう拡張されるのかを探ることにあります。

基礎：ランベック計算

1958年に提唱されたこの体系は、交換則・弱化則・縮約則を持ちません。つまり、語の「順番」と「個数」を厳密に管理します。

ϕ := ϕ / ϕ ∣ ϕ ∖ ϕ ∣ α

解析例：Alice runs

Aliceを $n p$ 、runsを $n p ∖ s$ とすると、以下の証明により文の正当性が保証されます。

\begin{matrix} \begin{matrix} n p \Rightarrow n p & s \Rightarrow s \end{matrix} \\ n p, n p ∖ s \Rightarrow s \end{matrix}

提案体系 $L μ$ と循環証明の導入

提案体系 $L μ$ では、再帰的な定義を扱うための最小不動点 ( $μ$ ) と、選択を行うための連言 ( $\land$ ) を追加しました。

ϕ := ϕ / ϕ ∣ ϕ ∖ ϕ ∣ ϕ \land ϕ ∣ μ X . ϕ_{X} ∣ α

推論規則と大域的トレース条件 (GTC)

不動点を展開する規則を追加します。ただし、論理的整合性を保つため、「すべての無限パスにおいて、左辺の $μ$ が無限回展開（unfold）される」という 大域的トレース条件 (GTC) を課します。

Left Rule ( $μ L$ ):

\begin{matrix} \begin{matrix} Γ, α [μ X . α / X], Δ \Rightarrow γ \end{matrix} \\ Γ, μ X . α, Δ \Rightarrow γ \end{matrix}

Right Rule ( $μ R$ ):

\begin{matrix} \begin{matrix} Γ \Rightarrow α [μ X . α / X] \end{matrix} \\ Γ \Rightarrow μ X . α \end{matrix}

応用：一般化された等位接続

$L μ$ では、"A, B, and C" のような可変長の接続をオートマトン的な挙動として記述できます。型を $χ \equiv (μ Y . Y \land X)$ および $τ_{a n d} \equiv (μ Y . (X ∖ X) \land (X ∖ Y)) / X$ と定義した際の証明構造は以下の通りです。

\begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} χ, τ_{a n d}, X \Rightarrow X (Backlink) \end{matrix} \\ χ, τ_{a n d}, X \Rightarrow X \end{matrix} & \begin{matrix} \begin{matrix} X \Rightarrow X & χ, X, (X ∖ τ_{a n d}), X \Rightarrow X \end{matrix} \\ χ, X, (X ∖ τ_{a n d}), X \Rightarrow X \end{matrix} (μ L) \end{matrix} \\ χ \land X, (X ∖ τ_{a n d}), X \Rightarrow X \end{matrix} (∖ L) \end{matrix} \\ χ, (X ∖ X) \land (X ∖ τ_{a n d}), X \Rightarrow X \end{matrix} (\land L_{2}) \end{matrix} \\ χ, τ_{a n d}, X \Rightarrow X \end{matrix} (μ L)

矛盾の定義

$L μ$ では「終わらない再帰」として矛盾 $⊥ \equiv μ X . X$ を定義可能です。これは GTC を満たしつつ、爆発原理（任意の命題の導出）を許容します。

\begin{matrix} \begin{matrix} ⊥ \Rightarrow ϕ (Backlink) \end{matrix} \\ ⊥ \Rightarrow ϕ \end{matrix}

結びに代えて

私の予想 (Conjecture) は、 「循環証明を入れても、言語クラスは文脈自由言語 (CFL) のまま変わらない」 というものです。交換則がないため交差依存を作れず、GTC により有限停止性が保証されるためです。今後は、無限ストリームを扱うための最大不動点 $ν$ を含む $L μ ν$ の構築を目指します。