💻 computer science

Cyclic Graphs and Memoization in Pure $\lambda$ -Calculus

本論文は、タブリングに基づく新しい操作意味論を用いることで、外部の再帰構文や不純なメモ化を必要とすることなく、純粋な $\lambda$ -計算が循環グラフ、自動的な動的計画法、および有限時間内でのループ検出をネイティブにサポートできることを実証するものである。

原著者： Bo Yang

公開日 2026-06-23

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Bo Yang

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

ビッグアイデア：数学の「魔法の鏡」

想像してみてください。そこには、純粋で抽象的な数学のルール（ $\lambda$ -計算と呼ばれます）があります。通常、これらのルールは厳格なレシピ本のようなものです。手順に従っていきますが、もしレシピが自分自身を呼び出していたら、本は「レシピ全体を何度も何度も書き出しなさい」と命じます。すると、無限に書き続けることになります。これには2つの大きな問題があります。

無限ループ： もし「ゼロのストリーム（0, 0, 0...）」を作ろうとしたら、数学は終わりのない紙の上に「0, 0, 0...」と書き続け続けます。それが単なる「円（ループ）」であることに気づけません。
無駄な労力： もし、同じ小さなパーツを何度も何度もチェックしなければならないパズル（例えば、2つの単語間の距離を計算するなど）を解こうとした場合、数学はそのパーツを毎回ゼロから計算し直し、サイズが爆発的に膨れ上がってしまいます。

論文による解決策：
著者は、これらの純粋な数学のルールを読み取りますが、答えの「書き方」を変える特別な「インタプリタ（翻訳機）」を作り上げました。単に答えを書き出すのではなく、**マップ（グラフ）**を構築するのです。

数学がループする場合、マップは「円」を描きます。
数学がステップを繰り返す場合、マップはすでに実行したステップへと戻る「矢印」を描きます。

魔法の正体は、数学のルールブックに新しいルールを一切追加することなく、これを実現している点です。これは「純粋」なままです。ただ、答えの表現方法を変え、無限の「木構造」を有限の「ループするマップ」へと変換しているだけなのです。

比喩 1：無限の廊下 vs 円形のトラック

問題点（従来の方法）：
「左に曲がって、この廊下を再び歩きなさい」という看板がある廊下を歩いていると想像してください。

標準的な数学： あなたは廊下を歩き、看板を見て、新しい廊下を歩き、また看板を見て、3番目の廊下を歩きます。あなたは決して止まりません。無限に長い廊下を作り続けているのです。
論文の方法： あなたは廊下を歩き、看板を見ます。そして新しい廊下を作る代わりに、現在の廊下の終点と始点を結ぶ線を床に描きます。これで、あなたは円形のトラックの上を走っていることになります。一度ここに来たことがあると認識できるので、新しい床を作るのをやめて、ループに従います。

なぜ重要か： 従来の方法では、廊下が無限になるため、紙（メモリ）が足りなくなります。新しい方法では、円を描くための1枚の紙があれば十分です。

比喩 2：働きすぎのシェフ vs 賢い副料理長

問題点（動的計画法）：
あるシェフが、2つの単語の「編集距離」（「kitten」を「sitting」に変えるために必要な変更回数）を計算しようとしているとします。

標準的な数学： シェフは最初の文字をチェックし、次に2番目、次に3番目と指示されます。しかし、3番目をチェックするために、シェフは2番目と1番目を再びチェックしなければなりません。それはまるで、玉ねぎを切るたびに、種から玉ねぎを育て、収穫し、それから切るという作業を繰り返すシェフのようなものです。同じ作業を何百万回も繰り返しています。
論文の方法： シェフには賢い副料理長（インタプリタ）がついています。シェフが初めて「玉ねぎ」を切る必要があるとき、副料理長がそれを実行し、「玉ねぎ」とラベルを貼ったボウルにそれを入れます。次にシェフが「玉ねぎ」を求めたとき、副料理長はただそのボウルを指差すだけです。
ひねり： この論文の主張は、シェフが副料理長に「これをやっておいて」と指示する必要はなかった、という点です。副料理長は、材料を見るだけで自動的にそれを理解しました。「メモ化（作業の記憶）」は、数学が「これは同じ材料を二度見ているのだ」と自然に認識したことによって起こりました。

比喩 3：無限ループの罠

問題点（不生産的なループ）：
時として、数学は役に立つものを何も生み出さずに回り続けるだけのループ（空回りする機械のようなもの）に陥ることがあります。

標準的な数学： 機械は永遠に回転し続けます。コンピュータは、決して訪れることのない結果を待ち続けるため、クラッシュしたりハングアップしたりします。
論文の方法： インタプリタは賢い監督者のようです。それは機械が回転する様子を見守ります。そして、「待て、君は5秒前にいた全く同じ場所に今戻ってきた。しかも、まだ新しい部品を一つも作っていないじゃないか」と判断します。監督者は緊急停止ボタンを押し、「これは壊れている」と言って、即座に「停止」信号（ $\bot$ ）を返します。これにより、コンピュータがハングアップするのを防ぎます。

これで何ができるのか？

この「マップ作成型」のインタプリタを使うことで、純粋な数学言語は、通常は「不純な（トリッキーな）コンピュータの手法」を必要とする強力なツールへと進化します。

動的計画法： 複雑なプログラム（ゲーム戦略や単語比較など）を、プログラマーが複雑な「これを覚えておけ」というコードを書かずとも、自動的に効率よく解くことができます。
循環データ： 特別な「再帰」コマンドを使わなくても、自分自身にループバックするデータ（循環リストなど）を作成し、操作することができます。
ゲーム探索： すでに見た盤面の状態を記憶することで、チェスや三目並べなどのゲームをプレイできます。これにより、同じ盤面を再計算して時間を無駄にすることがありません。
自己コンパイル： 著者は、このシステムを使って、この純粋な数学言語だけで書かれたコンパイラ（コードを翻訳するプログラム）さえも作成しました。そのコンパイラは、自分自身をコンパイルできるのです！

「秘伝のソース」

この論文の核心的な主張は、ループを実現するために数学に「魔法のボタン」（letrec や Y など）を追加する必要はない、ということです。ただ、答えをどう見るかを変えるだけでよいのです。

古い視点： 答えは、展開されていく長い「木の構造」である。
新しい視点： 答えは、ステップが自分自身を指し示すことができる「グラフ」である。

数学を、ステップが「同一性（これは以前見たステップと同じか？）」を鍵とするグラフとして扱うことで、インタプリタは無限のループを有限の円へと折りたたみ、繰り返しを単一のステップへとまとめ上げます。これにより、純粋な数学言語を、純粋さを壊すことなく、グラフ計算のための実用的なツールへと変貌させるのです。

技術要約：純粋 $\lambda$ -計算における循環グラフとメモ化

1. 問題提起

標準的な操作意味論における純粋 $\lambda$ -計算は、外部的な拡張なしには、循環データ構造や無限計算を表現したり効率的に操作したりすることが根本的に不可能です。

循環データの表現: 標準的な簡約（例： $Y(\text{cons } 0)$ ）は、無限のストリームを有限の循環グラフへと折り畳むのではなく、無限の木（ $0, 0, 0, \dots$ ）へと展開してしまいます。有限のサイクルを得るためには、従来の方式では letrec や $\mu$ -バインダーのような再帰構造を追加する必要があります。
メモ化と動的計画法: 動的計画法（例：編集距離）やグラフ探索（例：循環リスト上のmap）を実装した純粋関数型プログラムは、指数関数的な時間計算量、あるいは非停止に陥ります。標準的な解決策には、メモ化のための可変キャッシュ、サイクル検出のための参照等価性プリミティブ、あるいは明示的な状態追跡データ構造といった、不純なメカニズムが必要です。これらは、純粋関数型言語の核心的な原則である参照透過性を損なうものです。
核心的な障害: 本論文は、通常の簡約には「ある項が以前に訪問されたかどうか」を認識するメカニズムが欠如していることを指摘しています。状態の同一性を純粋に検出する方法がなければ、計算体系は繰り返される部分問題を自動的に共有したり、無限の展開を有限のサイクルへと折り畳んだりすることができません。

2. 手法

著者らは、**タブリング弱ヘッド簡約（tabling weak-head reduction）**に基づく、純粋 $\lambda$ -計算の新しい操作意味論を提案しています。このアプローチは、計算体系への拡張（letrec や不純性の導入）を必要とせず、インタープリタが項を実行する方法を変更するものです。

2.1 タブリング弱ヘッド簡約

この手法は、以下の2つの概念を組み合わせたものです。

弱ヘッド簡約 (Weak-Head Reduction): インタープリタは、項の「一層」を、その直近の下位項に対する弱ヘッド正規形のトップコンストラクタとして露出させます。これが「一層のマップ」($out$) を定義します。
タブリング (状態の同一性によるメモ化): インタープリタは、簡約中に遭遇した状態（部分項）のテーブルを保持します。
- 状態の同一性: 状態は、de Bruijn 項のインターン化（interning/hash-consing）による構造的同一性によって識別されます。これは決定可能であり、定数時間のポインタテストです。
- 解決 (Resolution): 項に遭遇した際：
  - それが新しい状態である場合、インタープリタはその層を計算し、再帰します。
  - それがすでにテーブルにある再入された状態である場合、既存のエントリを再利用します。
  - それが現在スタック上に存在する再入された状態（バックエッジ）である場合、インタープリタは無限に展開するのではなく、グラフ内にサイクルを閉じます。

2.2 アルゴリズム

評価は、 $\bot$ （未定義）から最小不動点へのクリーン・イテレーション（Kleene iteration）を通じて進行します。

アルゴリズム1 (ドライバ): 項を反復的に解決します。計算された層を、深層マージ演算子（ $\sqcup$ ）を用いて実行中の近似値へとマージしていきます。項がスタック上で再入された場合、現在の近似値を返します（初期値は $\bot$ ）。
アルゴリズム2 (WHNF): 弱ヘッド正規形のための特定の「一層のマップ」です。コンストラクタ（変数、抽象、または適用）が露出するまで、ヘッド簡約を適用します。
アルゴリズム3 (エバリュエーター): ドライバとマップを合成します。これは、ノードが項を表し、エッジが部分項を表す、有限のグラフ（循環を含む可能性がある）を返します。

2.3 理論的基礎

健全性 (Soundness): エバリュエーターが返すグラフは、その項の Lévy–Longo 木へと展開されます。このグラフは、項の表示的意味論の有限な表現です。
一意性 (Uniqueness): 簡約が「ガードされている」（ルートが確定してから部分項が読み取られる）ため、解は一意です。これにより、エバリュエーターによって計算される最小不動点が、最大不動点（余帰納的な木）と一致することが保証され、結果は簡約順序に依存しません。
停止性 (Termination): もし項が有限個の異なる状態（構造的同一性）に到達する場合、エバリュエーターは有限の循環グラフと共に停止します。もし無限個の異なる状態に到達する場合、標準的な簡約と同様の挙動（潜在的な発散）を示します。

3. 主要な結果とケーススタディ

著者らは、この意味論をインタープリタ（Co-Lambda）として実装し、以下の3つの領域でその能力を実証しました。

動的計画法 (編集距離):
- 素朴には指数関数的な時間を要する編集距離の純粋 $\lambda$ 項が、$O(mn)$ の時間および空間で評価されます。
- インタープリタは、部分問題（接尾辞のペア）が構造的に同一のインターン化されたノードであるため、これらを自動的に共有します。ソースコード内に明示的なメモ化テーブルや既読セットを記述する必要はありません。「テーブル」はインタープリタの内部状態テーブルとして機能します。
- 結果: 指数関数的なコールツリーが、標準的なDPテーブルを表す有限のグラフへと収束します。
循環データ (ゼロのストリーム):
- 標準的な簡約では無限のゼロのストリームを展開してしまう項 $r = Y(\text{cons } 0)$ が、有限の循環グラフとして評価されます。
- インタープリタは、ストリームのテイルが現在の計算と同じインターン化されたノードであることを検出し、バックエッジを閉じることでサイクルを形成します。
- 結果: 項 $r$ は、無限のメモリ使用量を伴わずに、自己ループを持つ有限のグラフとして評価されます。
不生産的なループ ( $\Omega$ ):
- 項 $\Omega = (\lambda x. x x)(\lambda x. x x)$ は、コンストラクタの層を露出させることなく自身へと簡約し続けます。
- 標準的な簡約では発散します。タブリング・エバリュエーターは、層が露出しない状態でスタックへの再入を検出し、その状態が不生産的であることを特定し、有限時間内に $\bot$ を返します。
- 結果: インタープリタは、データが生成されない特定のループに対して非停止を判定します。

4. 貢献

構成: 循環的な無限木を有限の循環グラフへと自動的に折り畳み、不生産的なループを判定する、純粋 $\lambda$ -計算のためのタブリングベースの操作意味論。
理論: 健全性（グラフはLévy–Longo木へと展開される）、一意性（最小不動点＝最大不動点）、および停止性の境界（有限のグラフであることは、到達可能な状態が有限個であることと同値）の証明。
応用:
- グラフ計算のためのDSL: このインタープリタは、メモ化、トランザクション・テーブル（ゲーム探索）、および既読集合（グラフ到達可能性）が、状態の同一性の帰結として暗黙的に組み込まれたドメイン固有言語（DSL）として機能します。
- 自己コンパイル・コンパイラ: 著者らは、自身のソースコードをPythonへとコンパイルするブートストラップ・コンパイラ（純粋 $\lambda$ 項として記述されたもの）を構築しました。このコンパイラは、コンパイルプロセスを最適化するために同じタブリング機構（関数脱構文化/defunctionalization）を利用しており、インタープリタ版と比較して大幅な高速化（約5倍）とメモリ削減を実現しています。

5. 意義と主張

本論文は、「純粋さの代償」を以下の2つの方法で解消すると主張しています。

拡張の排除: 循環グラフやメモ化が、再帰構造（letrec）や不純なプリミティブ（ポインタ等価性）を言語に追加することなく達成できることを示しています。「認識」は項ではなく、ソルバー（インタープリタ）によって行われます。
有理的部分 (Rational Fragment): この計算体系は、「有理的」な計算（有限個の異なる部分木を持つ計算）のための小さなDSLとなります。これらの計算において、インタープリタは自動的な動的計画法とサイクル折り畳けを提供します。
限界: 本論文は「有理的な天井」があることを認めています。この手法は構造的同一性（決定可能）に依存しています。 $\beta$ 等価（ $\beta$ -equal）ではあるが構造的に異なる項を折り畳むことはできません（ $\beta$ 等価性は決定不能であるため）。したがって、これは有理的な断片を解決するものであり、あらゆる無限の振る舞いの全空間を解決するものではありません。

本研究は、 $\lambda$ -計算を単なる命令的な計算（ステップバイステップの簡約）を行う言語としてではなく、宣言的な計算（構築されるべきグラフを指定する）を行うための言語として再定義しています。そこでは、ソルバーがグラフ構築の効率性と停止性を処理します。