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

2025年12月19日、数理論理学の集会であるMLG60にて、「ランベック計算の循環証明体系 $L μ$ の試み」というタイトルで発表を行いました。本記事では、その発表内容を振り返りつつ、ランベック計算 (Lambek Calculus) という言語学的な動機を持つ論理体系に循環証明 (Cyclic Proof) を導入することで何が見えてくるのか、そしてそれが形式言語理論（オートマトンと言語の理論）においてどのような意味を持つのかについて解説します。

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

なぜ今、ランベック計算なのでしょうか？その背景には、論理体系と形式言語のクラス（チョムスキー階層）の間に見出されている、非常に綺麗な対応関係があります。近年、以下のような階層構造が整理されつつあります。

通常の Lambek Calculus ( $L$ ) は文脈自由文法 (CFG) と等価であり、論理式の深さを制限した Shallow Lambek Calculus は線形文法 (Linear Grammar) に対応します。さらに、演算子を一方に制限した Simplified Shallow Lambek は正規文法 (Regular Grammar) に対応することが知られています。このように、論理側の制約を強めることで、対応する文法クラスの計算能力も制限されていくという図式があるのです。本研究の目的は、この図式に「循環（サイクル）」、すなわち無限の証明構造を導入した $μ$ -Lambek calculus ( $L μ$ ) を加えることで、この階層がどう拡張されるのかを探ることにあります。

まずは、基礎となるランベック計算について簡単に振り返っておきましょう。これは1958年に Joachim Lambek によって提唱されたもので、自然言語の統語論（Syntax）を証明論の枠組みで捉えようとする試みです。この論理の最大の特徴は、交換則・弱化則・縮約則を持たないという点にあります。つまり、命題（単語）の「順番」と「個数」を厳密に管理するのです。原子論理式（ $α$ ）からなる論理式の集合は、以下のように帰納的に定義されます。ここで、 $A ∖ B$ は「左に $A$ を取って $B$ になる型」を、 $A / B$ は「右に $B$ を取って $A$ になる型」を表します。

φ : = φ / φ ∣ φ ∖ φ ∣ α

推論規則としては、以下のような公理、カット、および論理規則（ $∖ L, ∖ R, / L, / R$ ）を持ちます。ここで、各記号は以下のような役割を持ちます。

$Γ, Δ, Σ$ ：論理式の有限の並び（文脈）を表します。
$α, β, γ$ ：個別の論理式（型）を表します。
$\Rightarrow$ ：左辺の並びから右辺の型が導出可能であることを示すシーケントです。
カンマ ( $,$ )：論理式の並びを結合します。非交換的な体系であるため、順番が重要です。

\begin{matrix} \begin{matrix} Γ \Rightarrow α & Δ, β, Σ \Rightarrow γ \end{matrix} \\ Δ, Γ, α ∖ β, Σ \Rightarrow γ \end{matrix} (∖ L) \begin{matrix} \begin{matrix} α, Γ \Rightarrow β \end{matrix} \\ Γ \Rightarrow α ∖ β \end{matrix} (∖ R)

\begin{matrix} \begin{matrix} Γ \Rightarrow α & Δ, β, Σ \Rightarrow γ \end{matrix} \\ Δ, β / α, Γ, Σ \Rightarrow γ \end{matrix} (/ L) \begin{matrix} \begin{matrix} Γ, α \Rightarrow β \end{matrix} \\ Γ \Rightarrow β / α \end{matrix} (/ R)

具体的な解析例として、「Alice runs」という文を考えてみましょう。Aliceを $n p$ （名詞句）、runsを $n p ∖ s$ （左に $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)

逆に、「runs Alice」という語順では、シーケントが $n p ∖ s, n p \Rightarrow s$ となり、証明ができず「非文」として弾かれます。

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

さて、ここからが本題です。従来のランベック計算は有限の証明木しか持ちませんでしたが、ここに循環証明 (Cyclic Proof) の枠組みを導入します。循環証明とは、証明木の中にループ（バックリンク）を許容することで、無限に続く証明構造を有限のグラフとして表現する手法です。今回提案する体系 $L μ$ では、通常のランベック計算に、再帰的な定義を扱うための最小不動点 ( $μ$ ) と、文脈に応じた選択（分岐）を行うための連言 ( $\land$ ) を追加しました。

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

これに伴い、不動点を展開するための規則（ $μ L, μ R$ ）や、選択を行うための規則（ $\land L, \land R$ ）が追加されます。

注：　発表中では連言の導入が必要であると判断し話しましたが、その後、循環証明体系の専門家との議論により必要ではないと判明しました。ここに訂正いたします。なお、余計な拡張というだけであり、真性の損失はないことを付記いたします。

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

\begin{matrix} \begin{matrix} Γ, α_{i}, Δ \Rightarrow γ \end{matrix} \\ Γ, α_{1} \land α_{2}, Δ \Rightarrow γ \end{matrix} (\land L_{i}) \begin{matrix} \begin{matrix} Γ \Rightarrow α & Γ \Rightarrow β \end{matrix} \\ Γ \Rightarrow α \land β \end{matrix} (\land R)

ただし、無制限にループを許すと論理が崩壊してしまうため、大域的トレース条件 (Global Trace Condition: GTC) という制約を課します。これは、「すべての無限パス $π$ に対して、そのパス上で左辺にある最小不動点 $μ$ が無限回展開 (unfold) されるようなトレースが存在しなければならない」というものです。直感的には、再帰的な定義（ $μ$ ）が無限に展開される際に、その構造が適切に消費・分解されていることを保証しています。

この拡張によって、言語モデルとしての表現力がどのように向上するのでしょうか。一つの面白い応用例として、一般化された等位接続 (Generalized AND) の表現が挙げられます。自然言語の “and” は、「A and B」のように2つを繋ぐこともあれば、「A, B and C」のように3つ以上を繋ぐこともあります。これらを有限個の型で統一的に扱うことは従来困難でした。しかし、 $L μ$ では、再帰 ( $μ$ ) と選択 ( $\land$ ) を組み合わせることで、これを解決できます。

型を $χ \equiv (μ Y . Y \land X)$ および $τ_{a n d} \equiv (μ Y . (X ∖ X) \land (X ∖ Y)) / X$ と定義し、これらを証明図に起こすと、以下のように「継続 (Cont) するか、終了 (Stop) するか」を $\land$ で選びながら、スタックされた $X$ を順次消費していくオートマトンのような挙動を論理式として記述できるのです。

\begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} \begin{matrix} χ, τ_{a n d}, X \Rightarrow X (Backlink) & 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} (\land L_{2}) \end{matrix} \\ χ, (X ∖ X) \land (X ∖ τ_{a n d}), X \Rightarrow X \end{matrix} (μ L) \end{matrix} \\ χ, τ_{a n d}, X \Rightarrow X \end{matrix} (μ L)

また、オリジナルのランベック計算には否定や矛盾といった概念が希薄ですが、 $L μ$ では「終わらない再帰」として矛盾 $⊥ \equiv μ X . X$ を自然に定義できます。左辺にこれがあると、証明図の中で無限に展開し続けることができるため、GTCを満たしつつ任意の命題を導出（爆発）させることができます。

\begin{matrix} \begin{matrix} ⊥ \Rightarrow φ (B a c k l i n k) \end{matrix} \\ ⊥ \Rightarrow φ \end{matrix} (μ L)

結びに代えて：今後の展望

最後に、この $L μ$ が形式言語理論のどのクラスに対応するかという議論ですが、私の予想 (Conjecture) は、「循環証明を入れても、言語クラスは文脈自由言語 (CFL) のまま変わらない」というものです。その根拠として、縮約則がないため計算リソースを勝手に増やせないこと、交換則がないため文脈自由文法を超えるような複雑な交差依存関係を作れないこと、そしてGTCにより有限ステップでの停止が保証されることが挙げられます。

今回は「最小不動点 $μ$ 」に焦点を当てましたが、その双対である「最大不動点 $ν$ 」を導入すると、さらに世界が広がります。 $μ$ が「有限で終わること」を要請するのに対し、 $ν$ は「無限に続くこと」を許容します。これを導入すれば、無限に続くストリームデータ $a^{ω}$ などを解析する型システムとしてのランベック計算 ( $L μ ν$ ) が構築できるかもしれません。

\begin{matrix} \begin{matrix} Γ, α [ν X . α / X], Δ \Rightarrow γ \end{matrix} \\ Γ, ν X . α, Δ \Rightarrow γ \end{matrix} (ν L) \begin{matrix} \begin{matrix} Γ \Rightarrow α [ν X . α / X] \end{matrix} \\ Γ \Rightarrow ν X . α \end{matrix} (ν R)

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

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

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

結びに代えて：今後の展望

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