💻 computer science

Well-Scoped Locally Nameless Representation of Syntax

本論文は、Plotkin 型の束縛署名をパラメータとする Agda 向けの汎用的かつ適切に範囲が定められた局所的な名前付き構文表現を提示し、その単純な名付き構文に対する充足性をアルファ変換の観点から証明し、さらに例示を通じてその有用性を示す。

原著者： Andrew M. Pitts

公開日 2026-05-12

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

CC BY 4.0

原著者： Andrew M. Pitts

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

あなたが、内部で他の本を参照できる本が溢れる巨大で混沌とした図書館を整理しようとする司書だと想像してください。ある本には表紙にタイトル（『グレート・ギャツビー』など）が書かれていますが、他の本は特定のセクション内の番号付き棚（「3 番棚、2 列」など）でしか識別されません。

アンドリュー・ピッツによって書かれたこの論文は、この図書館のルールをコンピュータ（特に Agda のような「対話型定理証明系」）が混乱したり誤ったりすることなく検証できるような、より賢い整理方法を提案するものです。

以下に、この論文のアイデアを単純な比喩を用いて解説します。

1. 問題：「名前なし」対「名前あり」のジレンマ

コンピュータ科学者がコンピュータに言語（プログラミング言語や論理など）を教える際、変数に対処しなければなりません。

「名前あり」方式： すべての変数に x、y、z のような名前をつけます。人間には読みやすいですが、名前を交換するとコンピュータが混乱します（これを「アルファ変換」と呼ぶ問題です）。名前を変えれば x と y は同じものになるのでしょうか？
「名前なし」方式（ド・ブリュイン指数）： 名前を完全に使わず、「1 番目の変数」「2 番目の変数」のように、内側から外側に向かって数えるだけです。これはコンピュータには優れていますが、数字の羅列のように見えるため人間には最悪で、理解するのが困難です。

2. 従来の解決策：「局所的に名前あり」

数年前、研究者たちは**局所的に名前あり（Locally Nameless）**と呼ばれるハイブリッドなアイデアを考案しました。

自由変数（ループや関数の内部に束縛されていないもの）は、名前（x など）を維持します。
束縛変数（ループ内部のもの）は、数字（0、1 など）を使用します。

欠点： このシステムには「罠」があります。スコープと一致しない数字を持つ「破損した」項を作成できてしまうのです。例えば、「5 番棚へ行って」という本があるのに、現在いる部屋には棚が 3 つしかないような状況です。コンピュータは常に「この項は『局所的に閉じている（有効である）』か？」を確認しなければなりません。これは、司書が誰かが本を借りる前に、その本が正しい通路にあるか常に確認しなければならないようなもので、多くの追加的な証明作業を必要とします。

3. 新しい解決策：「スコープが適切に保証された局所的に名前あり」

この論文は、より優れた方法を提案します。**スコープが適切に保証された局所的に名前あり（Well-Scoped Locally Nameless）**です。

単に数字を使うのではなく、コンピュータはルールを強制するために型を使用します。

図書館を異なる「部屋」を持っていると想像してください。
部屋 0にいる場合、見ることができるのは 0 から 0 までの棚番号だけです（つまり棚はなく、自由な名前のみが存在します）。
部屋 1にいる場合、0 と 1 の棚が見えます。
部屋 5にいる場合、0 から 5 までの棚が見えます。

魔法： このシステムでは、破損した本を物理的に作成することができません。「部屋 2」に立っているのに「10 番棚へ行って」と書こうとすれば、コンピュータの型システムは「いいえ、それは不可能だ。その文を書くことさえできない」と言います。

この論文は、このアプローチが以下の点で優れていると主張しています。

「罠」の排除： 項が有効かどうかを確認するための追加証明を書く必要がありません。項が存在する事実そのものが、それが有効であることを証明します。
透明性： 人間が慣れ親しんだ「名前あり」方式とほとんど同じに見えるため、純粋な「名前なし」方式ほど混乱しません。
汎用性： 著者たちは、バインドのルール（if 文やラムダ関数の動作など）を標準的なテンプレートを使って記述さえすれば、定義したい任意の言語に機能する「ライブラリ」（ツールセット）を構築しました。

4. 仕組み（「開く」と「閉じる」）

この論文は、本を部屋間で行き来させるような 2 つの主要な操作を記述しています。

抽象化（閉じる）： 自由な名前（x など）を取り出し、束縛されたインデックス（0 など）に変換します。これは、本を棚から取り出し、新しい部屋の特定の番号付きスロットに入れるようなものです。
具体化（開く）： 束縛されたインデックスを取り出し、特定の項（本）に置き換えます。これは、スロットから本を取り出し、その場所に実在する本を置くようなものです。

著者たちは、彼らの「スコープが適切に保証された」数学が完璧に機能することを証明しました。彼らは、新しいシステムが従来の「名前あり」システムと数学的に等価であることを示しました。つまり、同じ概念を表しているのですが、より安全に整理されているのです。

5. 実世界の例

この論文は理論だけでなく、彼らの「ライブラリ」を 3 種類の異なる言語でテストしました。

π計算（Pi-Calculus）： コンピュータプログラムが互いに通信する方法（電話通話など）を記述するために使用される言語です。ここでは、名前は通信の「チャネル」となります。
マルティン＝レーフ型理論： 数学的証明のための複雑なシステムです。彼らは、名前の「鮮度（freshness）」に迷い込むことなく、自然数や型のルールを記述する方法を示しました。
ゲーデルの系 T： 計算が最終的に終了すること（決定性）を証明するためのシステムです。彼らはこの手法を用いて、特定のアルゴリズムが正しく機能することを証明しました。

結論

この論文はこう述べています。「変数が正しい場所にあるかどうかを手動で確認するのをやめましょう。コンピュータの型システムに重労働を任せてください。」

依存型（Agda プログラミング言語の機能）を使用することで、彼らは無効な構文を書き込むこと自体が不可能なシステムを構築しました。これにより、「はい、この変数はスコープ内です」と言うために、研究者が何千行もの退屈な証明コードを書く必要がなくなりました。これにより、形式検証（ソフトウェアにバグがないことを証明すること）は、より容易で安全になり、人間が言語について自然に考える方法に近づきました。

技術的概要：スコープが適切に定義された局所的に名前のついた構文の表現

問題定義
依存型理論に基づく対話的定理証明系（Agda、Lean、Rocq など）において、束縛構文（ $\lambda$ -計算や型システムなど）を持つ言語を形式化する際、変数の束縛と $\alpha$ -同値の管理が中心的な課題となります。「局所的に名前のついた（locally nameless）」アプローチは、自由変数を明示的な名前として、束縛変数を de Bruijn 指数として表現するものであり、低いインフラコスト、透明性、参入の容易さという PoplMark 基準を満たすことが示されています。しかし、標準的な局所的に名前のついた表現には致命的な欠陥があります。それは、項の帰納的定義が「浮遊する（dangling）」指数（現在のスコープを超える指数）を許容してしまう点です。正しさを保証するためには、定義域を「局所的に閉じた（locally closed）」項の部分集合に制限する必要があります。これにより、置換などの操作が局所的閉性を保持することを示すための反復的で手作業による証明が必要となり、形式開発において大きな負担と潜在的な誤りの源泉となっています。

手法
本論文は、Agda の依存型システムを活用して、局所的閉性を別個の述語としてではなく、本質的に強制する「スコープが適切に定義された（well-scoped）」局所的に名前のついた表現のバリアントを提案します。

インデックス付き帰納型: 単一の項の型ではなく、自然数 $n$ でインデックス付けられた型の族 Trm[n] を定義します。 $n$ -項とは、すべての de Bruijn 指数が有限型 Fin n（ $n$ 未満の自然数）から選ばれている項です。
0-項としての局所的に閉じた項: この枠組みにおいて、「局所的に閉じた」項（浮遊する指数を持たない項）は、正確に Trm[0] に対応します。自由変数を持つ項は、スコープ内の自由変数の数に対応する $n$ に対して Trm[n] として表現されます。
束縛シグネチャによるパラメータ化: 本ライブラリは汎用的であり、Plotkin 風の束縛シグネチャによってパラメータ化されています。これにより、演算子、そのアリティ、および各引数位置で束縛される名前の数を定義することが可能になります。
依存型による操作:
- スコープの弱化（Scope Weakening）: 指数を注入し、より大きなスコープへ移動する際に必要なシフトを処理する関数 Trm[m] -> Trm[n]（ $m \le n$ の場合）。
- 具体化（Opening）: $(1+n)$ -項内の指数 $i$ を 0-項に置き換えて $n$ -項を生成すること。これには $i$ より大きい指数を 1 つ下げる処理が含まれます。
- 抽象化（Closing）: $n$ -項内の自由な名前を指数に置き換えて $(1+n)$ -項を生成すること。これには指数を上げる処理が含まれます。
- 置換: 構造的に定義されます。置換関数は名前を 0-項（Trm）に写像するため、「局所的に閉じた」という条件は型システムによって自動的に強制されます。 $n$ -項に対する置換は、別の $n$ -項を生成します。

主要な貢献

WSLN ライブラリ: スコープが適切に定義された局所的に名前のついた項を実装する汎用 Agda ライブラリ。Plotkin 束縛シグネチャによって指定される任意の言語について、構文、操作（弱化、置換、抽象化、具体化）、および推論原理を定義するためのインフラを提供します。
形式的妥当性の証明: 以下の 2 つの間の全単射を確立する厳密な証明を提供します。
1. スコープが適切に定義された局所的に名前のついた 0-項の型（Trm[0]）。
2. 「名前のついた（nameful）」項（自由変数と束縛変数の両方に明示的な名前を持つ項）の $\alpha$ -同値類。
  この全単射は、スコープが適切に定義された表現が、捕捉を回避する置換と $\alpha$ -同値のセマンティクスを正しく捉えていることを示しています。
局所的閉性証明の排除: スコープ制約を型のインデックスに符号化することで、「局所的に閉じた」述語の明示的な定義と、それに関連する証明義務（例えば、置換が局所的閉性を保持することを証明すること）を排除します。これらの性質は、型付け規則の結果となります。
鮮度（Freshness）の処理: 本ライブラリは名目的手法（nominal techniques）と統合され、自然数という「有限に無限ではない（finitely inexhaustible）」集合を用いて、余有限量化（cofinite quantification）を通じて新しい名前を生成します。これにより、鮮度の条件が体系的に処理されます。

結果
本論文は、Agda で実装された 3 つの異なる例を通じて、このアプローチを検証します。

$\pi$ -計算: $\lambda$ -計算を超えてライブラリが適用可能であることを示し、プロセス式とチャネル名を扱います。ライブラリが束縛構造を処理する一方で、正当性の型チェック（例えば、チャネルが期待される場所で使用されていることを保証すること）は、別途ユーザーが定義する判断であることを強調しています。
Martin-Löf 型理論（MLTT）: ライブラリが型付け規則の定義をどのように容易にするかを示します。「存在する鮮度（exists-fresh）」規則（明示的な鮮度の仮定を必要とする）と「余有限量化」規則（鮮度が暗黙的である）を対比させ、スコープが適切に定義された表現が後者をサポートし、よりクリーンで透明な形式化につながることを示しています。
ゲーデルのシステム T（評価による正規化）: $\beta\eta$ -変換の決定可能性を証明する大規模な開発です。この例は、スコープが適切に定義された表現が、抽象化のセマンティクスと、複雑な意味論的構成（集合値前層）における鮮度の処理をどのように簡素化するかを示しており、有限サポートを持つ意味論的対象の必要性を回避しています。

意義と主張
本論文は、スコープが適切に定義された局所的に名前のついた表現が、従来の局所的に名前のついたアプローチに見られる「浮遊する指数の罠」に対する「直接的」かつ強力な解決策を提供すると主張しています。その主な意義は、スコープの正しさを保証する負担を、ユーザー（手作業による証明を通じて）から、定理証明器の型チェック器（依存型を通じて）へと移行させる点にあります。

著者は、このアプローチが PoplMark 基準が要求する透明性を維持していると強調しています。形式的な定義は非公式な慣習に密接に反映され、「指数ヨガ（de Bruijn 指数の操作）」はライブラリの操作にカプセル化されています。実装には有限順序数（Fin n）と指数シフトの慎重な処理が必要ですが、ライブラリはこの複雑さをパラメータ化しており、ユーザーは低レベルのスコープメカニクスを管理することなく、言語を定義し、性質を証明することができます。本論文は控えめに、現在の束縛シグネチャはソートされておらず単純な束縛スコープをモデル化しているものの、システム T の開発が示すように、このアプローチは複雑な型システムや意味論的証明を処理するのに十分な頑健性を持っていると述べています。