RFC-027a: 停止性検査の明示的測度

概要

RFC-027 §7 は停止性検査の判定基準を精化型（精化は検証モードへの進入）と定め、§6.9 で明示的測度の言語形式（組み込み述語 Terminates、Int、Never と同じ中核プリミティブ）を提示している。どちらも言語設計であり、ホスト RFC として確定済みである。

本子 RFC は実装メカニズムを引き継ぐ：義務が計算構造からどう生成されるか、判定パイプラインがどう編成されるか、証明できない時に診断がどう方向を示すか、相互再帰の測度がどう共有されるか（SCC 最適化）、エラーコードがどう登録されるか。言語意味論は繰り返さず、メカニズムのみを定める。

動機

なぜ子 RFC が必要か

判定基準（精化型検証モードへの進入）と形式（Terminates を型位置に記述）は RFC-027 で確定済みであり、粒度は言語レベルである。残った問題は粒度が細かすぎて、ホストに書くと本文が肥大化する：

• 義務の出所（再帰呼び出し点、ループの逆辺、パスガード）
• 測度がタプルを返す場合の比較方法（辞書順展開）
• 整礎性と厳密減少は独立した2つの義務か、統合か
• 自動探索と明示的測度が同一パイプラインにどう共存するか
• 相互再帰時に同一測度の重複記述と重複検証をどう避けるか
• 証明できない時に方向をどう示すか（単なる拒否ではなく）

トリガー

方向は #318 がトリガー：非構造再帰（gcd 型の非直接減少、相互再帰、マージ分割）は測度探索のテンプレート列（RFC-027 §6.2–6.5 の4戦略はいずれも「有界型の変数」または「目標型 + 交換操作」を入力とする）を超え、可読性を損なわずに分析可能な反復パターンに書き換えられない。RFC-027「オープン問題」節の再検討条項がここで発動する。

提案

自動探索との関係

明示的測度は別のパイプラインではなく、探索失敗後の入力である。測度を与えても同一の SMT が同一の義務群を検証する；不成立ならエラーと反例を返す。全自動優先は変わらない：探索が常に先に走り、ユーザーの介入は探索失敗後にのみ発生する。

これにより2つの経路が下流メカニズムをすべて共有する——義務生成、SMT 判定、辞書順展開、診断フォーマットは実装が1つだけになる。

義務生成

関数 f と測度 m に対し、独立した2つの義務を生成し、再帰呼び出し点（SCC 内の関数間呼び出しを含む）ごとに展開する：

1. 整礎性：m(args) >= 0——測度は自然数上にある；測度が非自然数型を返す場合、その型上の適切な順序の下限を取る。引数の精化から導出し、できない場合は残余義務に入る。
2. 厳密減少：各呼び出し点で m(callee_args) < m(caller_args)、パスガード下で判定——ガードはその呼び出し点が属する分岐条件から得られ、RFC-009a のパス条件収集を再利用する。

2つを統合せず独立させる理由は、失敗の方向が異なるため：整礎性の失敗は測度の値域が不適切（例：Int は負になり得る）であることを示し、減少の失敗は再帰引数がその方向に進んでいないことを示す。診断は両者を区別し、正しい検査方向を示す必要がある（「診断」節参照）。

ループも同様で、「呼び出し点」を「逆辺」に置き換える：ループ本体の各実行パスで m(次の状態) < m(現在の状態)、ガードはループ条件と本体内の分岐から得られる。

辞書順展開：m がタプル (m₁, …, mₖ) を返す場合、義務は辞書順比較で選言連鎖に展開される——(m₁' < m₁) ∨ (m₁' == m₁ ∧ m₂' < m₂) ∨ …。展開は義務生成側で完了し、SMT 側は線形フラグメントを保持し、ソルバーの辞書順ネイティブサポートに依存しない。

測度自体はコンパイル時に評価可能でなければならない：m は定数畳み込みまたは構造再帰で証明可能な関数でなければならない——停止性問題を別の未証明関数に再帰的に委ねることを禁止する（無限後退の防止）。病的測度は既存の E4012（定数再帰の過度な深さ）と構造検査で阻止される。

判定パイプライン

1. 仮引数減少（構造再帰、最も強いパス、先に試す）
2. 測度探索：4戦略テンプレート列（RFC-027 §6.2–6.5）、1つ見つけたら停止
3. 探索成功 → 義務生成 → SMT 判定 → Proved
4. 探索失敗 → 型位置に明示的測度（Terminates）があるか確認
     有り → その測度で義務生成 → SMT 判定
     無し → E4021（停止性を証明できない、推奨検査方向を添付）
5. 義務が SMT で反証される → E4022（測度が不成立、反例を添付）

1–3 段は RFC-027 既定パスであり、本 RFC は第4段と2つのエラーコードを新たに追加する。パイプライン全体は精化型がトリガーされた時のみ実行される（RFC-027 §7）——精化無しの通常型は義務を一切生成しない。

アンカー：単項形式と二項形式

RFC-027 §6.9 は2つのアリティを定めたが、本 RFC はそれぞれの落とし所を説明する：

形式	アンカー	落とし所
Terminates(m)	所在の束縛名	定義箇所のデフォルト形式——自己再帰関数、ループ
Terminates(FnType, m)	明示的な関数型	測度の帰属を明示する必要がある場合（測度が別所で定義、同一測度が複数の計算に提供）

両者は2つの構成ではなく、同一述語の2つのアリティである：停止性義務は常に「精化の存在する型位置に注釈された計算」に位置する。相互再帰は二項形式を必須としない——2つの関数がそれぞれ単項形式で書けばよく、共有関係は SCC が識別する（次節参照）。

SCC：測度共有最適化

相互再帰する関数の組（呼び出しグラフの強連結成分）が同一測度を共有する場合、関数間の辺の義務は m_callee(callee_args) < m_caller(caller_args) であり、メンバーが測度を共有すると同一測度の減少に退化する。

これは最適化であり、正確性の前提ではない：共有しない場合は各関数がそれぞれ測度を書けば、独立して閉路して通る。SCC の価値は「この組は同一測度を使っている」を見抜き、重複記述と重複検証を省くことにある。

関数レベル呼び出しグラフと SCC 収集を新規作成する必要がある——既存の TypeDepGraph は変数間の型注釈依存（RFC-027 §6.1 の VC トリガー）を記録する変数レベルグラフであり、再利用不可。

例

gcd：非構造再帰

// 測度：通常関数、単体テスト可、再利用可
gcd_measure: (a: Int, b: Int) -> Int = { b }

gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

義務生成：

1. 整礎性：gcd_measure(a, b) >= 0 すなわち b >= 0——仮引数精化 NonNegative(b) から直接導出
2. 厳密減少：唯一の再帰呼び出し点 gcd(b, a % b)、パスガード b != 0、義務 gcd_measure(b, a % b) < gcd_measure(a, b)；測度の本体を代入して展開すると a % b < b
3. SMT：否定 b != 0 ∧ a % b >= b の充足不能を検証 → Proved

ループ：匿名構造の指示対象の取得

loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n {
        i = i + 1
    }
    return acc
}

Terminates(m) の精化はループ本体の末尾式の値型であり、アンカーは束縛名 acc が提供する——したがってループは指示対象を持ち得る、「匿名構造に指示対象が無い」死角はなくなる。これは2つのアリティの統一性も説明する：義務は常に精化の存在する型位置に注釈された計算に位置し、関数とループに区別はない。

義務：逆辺上で (n - i') < (n - i)、ガード i < n、i' = i + 1 を代入すると 1 > 0、常に真 → Proved。

相互再帰：SCC 共有測度

nat: (n: Int) -> Int = { n }

is_even: Terminates(nat) = {
    if n == 0 { return true }
    return is_odd(n - 1)
}
is_odd: Terminates(nat) = {
    if n == 0 { return false }
    return is_even(n - 1)
}

2つの関数はそれぞれ単項形式の Terminates(nat) を持つ。SCC 収集後に2者が同一測度を共有していると識別され、関数間辺の義務 nat(n - 1) < nat(n) はガード n != 0 下で常に真であり、2関数とも1度の検証で閉路する。

SCC 識別を行わなくても、2関数がそれぞれ同一義務を検証すれば依然として通る——重複が一度あるだけだ。これが SCC の位置付けが最適化であることの証拠。

診断

整礎性が証明できない時は直接拒否せず、検査方向を提案する。 これは減少義務失敗の診断と区別する必要がある：前者は測度の値域を指し、後者は再帰引数を指す。3種類の失敗それぞれの提案：

失敗	提案方向
整礎性が証明できない	測度が取り得る値の下限を成立させているか（例：Int 測度に >= 0 が必要か）
厳密減少が反証される	再帰引数が実際に測度の減少方向に進んでいるか；SMT 反例を添付
測度無しで探索失敗	当該計算に名前を束縛し型位置に測度を提供できることを示唆（RFC-027 §6.9）

反例表示は RFC-013 診断メッセージ仕様に従う。非線形のパスガード下では Sat 反例が直感的でない場合がある——既知の制限として記録し、RFC-013 の反復で対応する。

エラーコード

E4xxx 証明失敗ファミリ（E4018 精化述語違反、E4020 証明関数を要求）に揃える：

提案コード	名前	トリガー
E4021	停止性を証明できない	探索失敗かつ型位置に明示的測度が無い（Terminates 測度の提供を示唆）
E4022	測度不成立	測度義務が SMT で反証される（反例を添付）

最終番号は実装時の RFC-013 レジストリ現況に従う（セグメントの合法性は build.rs 閾値で保証）。

診断層の既存欠陥

現行実装では、スコープ内の停止性失敗は E8001「内部コンパイラエラー」 として報告される（Unproven が ICE としてフォーマットされる）——停止性検査は ICE ではなく、このコード位置を占有することはユーザーを誤誘導し真の障害を隠蔽する。本 RFC で一括修正する：スコープ内の停止性失敗は E4021/E4022 を経由し、ICE コード位置は真の内部エラーに返還する。

コンパイラの変更

コンポーネント	変更
typecheck/layers/termination.rs	インターフェースの統一（探索パスと明示的測度パスで義務生成と判定を共有）；Z3 の接続（本番パイプラインへの注入、with_z3 は現在単体テストのみ）
関数呼び出しグラフ + SCC（新規作成）	リポジトリ全体に関数間呼び出しグラフが存在しない——TypeDepGraph は変数レベル型依存であり、再利用不可。関数レベル呼び出しグラフと SCC 収集を新規作成し、相互再帰の測度共有に使用
義務生成	追加：整礎性/厳密減少の2つの義務、パスガードの注入、辞書順展開
証明パイプライン（RFC-009a / #292）	ConstExpr → SMTLib パイプラインと Mod 等の演算子マッピングを再利用、バックエンド変更なし
util/diagnostic/codes/e4xxx.rs	E4021/E4022 登録を追加（RFC-013 レジストリ経由、build.rs 閾値発効）
locales ×6	2つの新コードの6言語テンプレート
診断層	スコープ内の停止性失敗を E8001 から移行し、証明失敗ファミリに変更

後方互換性

• これまで停止性検査で拒否されたが精化注釈の無いプログラム：新判定基準では検証モードに入らず、直接コンパイル成功——意図的な緩和、緩和のみ、厳格化なし。
• これまで停止性検査で拒否され、かつ精化注釈のあるプログラム：測度を補えば通過可能。
• 構造再帰の正例、既存の停止性テスト：期待出力は不変。

トレードオフ

利点

• 新規構文ゼロ：測度は型位置に記述し、精化述語適用メカニズムを再利用；decreases 系の構文位置なし。
• 証明領域の動作整合：停止性領域に正確性領域と一貫したフォールバック経路を補完するが、落とし所は異なる——正確性領域で証明できない命題は本体に証明関数を記述し、停止性領域の探索で得られない測度は型位置で宣言する。両者のメカニズムは同一（いずれも精化型の適用）。
• インフラの再利用：義務は線形算術とパスガードで、#292 で既に接続されたパイプラインを走行、新規バックエンドなし。
• ループの指示対象化：束縛名がそのままアンカーとなり、ループと関数は義務生成上完全に同型であり、ループ専用の特例設計は不要。

欠点とリスク

• 「配線」に必要な事前インフラ量は少なくない：関数レベル呼び出しグラフと SCC 収集は新規作成が必要、Z3 も本番パイプラインに未接続。SCC 部分は延期可能（最適化）だが、呼び出しグラフ部分は SCC と同源のため、延期すると相互再帰は各々が測度を書くことになる——それでも通るが、重複検証。
• 明示的測度は低頻度パスの記述負担：2点セット（測度関数 + 型位置宣言）はインライン注釈より冗長。受け入れる——フォールバックは低頻度パスであり、測度の再利用可能性と単体テスト可能性と引き換え。
• 整礎性義務のノイズ：測度が Int を返す場合、毎回 >= 0 を証明する必要がある。緩和策：引数精化に既に下限があれば自動導出；できない場合のみ残余義務に入り、方向のみを示し拒否しない。
• 反例の品質：非線形ガード下での Sat 反例は直感的でない。既知の制限。
• Terminates はコンパイラが本体を代筆する唯一の述語：「述語本体は全てユーザーが記述可能」という純粋性から逸脱する。理由：その表明（各呼び出し点/逆辺の測度減少）は計算構造内に位置し、ユーザーが記述した述語は関数本体やループ本体を参照できない。組み込み面が1つの名前に集約され、メカニズムの追加はゼロ。

代替案

• with decreases (b) インライン注釈構文：本 issue の初期提案で撤回済み。「停止性検査に注釈構文の入口は設けない」は RFC-027 の確定した意思決定であり、インライン注釈は未対応の終了モードを構文位置にし、型位置にしないことで「すべてが YaoXiang 関数、すべてが型チェッカーで検証される」という世界観と相いれない。
• 独立した証明関数（gcd_proof が Terminates(f, m) を返し、戻り型をスキャンして発見）：初期設計。廃止——「発見メカニズム」「命名規約」「複数候補から最初を選択」「証明関数本体内の名前解決方法」の4種類の複雑さをもたらすが、これらは全て証明を体外に置いたためである。型位置に記述する形式に変更後、4種類の複雑さはすべて消える。
• 測度のみを型に組み込む（Terminates(m)）、二項形式を廃止：より短いが、「明示的に測度の帰属を指定」する表現位置を失う（測度が別所で定義、同一測度が複数の計算にサービスを提供する場合の置き場がない）。2つのアリティは同一述語の2つのアリティであり、保持コストはほぼゼロ。
• フォールバックを行わず、ユーザーに分析可能な反復パターンへの書き換えを要求：すなわち現状。gcd / マージ分割 / 相互再帰は可読性を損なわずに書き換えられない——これがまさに再検討条項の発動条件。

非目標

• 新規構文/キーワード/注釈位置を追加しない。
• 測度の自動合成の汎用化拡張は行わない（4戦略は RFC-027 既定計画を維持、射程外は明示的測度で対応）。汎用測度推論は「発見」の決定不能側に属し、テンプレートの境界のみ約定でき、完備性は保証できない。
• RFC-009a と命題の連立求解を借用しない（それぞれ独立して判定し、バックエンドを共有）。
• 依存型レベルでの totality checking は行わない。
• 測度に自然数型を返させる強制はしない（Lean の WellFoundedRelation 型クラスメカニズムを追求しない）——測度の戻り型は制約なし、整礎性は独立義務として精化導出または SMT に委ねる。

段階と受け入れ基準

• [ ] 義務生成（整礎性/厳密減少、パスガード注入、辞書順展開）
• [ ] 明示的測度の配線（Terminates 単項と二項形式のアンカー解析、型位置からの測度抽出）
• [ ] SMT 判定の配線（#292 パイプラインの再利用、本番パイプラインへの Z3 注入）
• [ ] 関数レベル呼び出しグラフ + SCC 収集（測度共有最適化）
• [ ] E4021/E4022 登録 + 6言語ロケール
• [ ] 診断層修正：スコープ内の停止性失敗を E8001 から移行し、証明失敗ファミリに変更
• [ ] E2E：正例（gcd / ループ Terminates(n - i) / is_even-is_odd 相互再帰）/ 負例（測度不成立 → E4022；測度なし → E4021）/ 構造再帰ゼロ回帰
• [ ] 判定基準回帰：精化注釈のない再帰とループは停止性検査で拒否されない；精化注釈がある場合、義務は通常通りトリガー
• [ ] 受け入れデモ：測度が成立しない宣言を書く → コンパイル失敗かつ反例が可読；修正後通過

関連

• #318（本 RFC の立上げ issue）、#251（親マイルストーン P1）
• RFC-027（ホスト：§7 精化型判定基準、§6.1–6.5 測度探索4戦略、§6.9 明示的測度、§オープン問題 再検討条項）
• RFC-009a / #292（SMT パイプラインとパス条件収集の共有——インフラ前提）
• RFC-013（エラーコードレジストリと証明失敗意味ファミリ）