論文「WHEN EQUALITY FAILS AS A REWRITE PRINCIPLE」の技術的サマリー

本論文は、計測データを含む数式（measurement-bearing expressions）における代数的な等式の書き換え（リライト）が、なぜ安全ではない場合があるかを形式的に分析し、その解決策となる統一的な意味論フレームワークを提案するものです。著者らは、**「出所（Provenance）」と「定義域（Definedness）」**の 2 つの側面を同時に追跡する必要があることを示し、これらを組み合わせた新しい書き換え判定基準を構築しました。すべての定義と定理は、Lean 4 において「sorry（未証明）」なしで形式化されています。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳述します。

1. 問題定義：等式が書き換え原理として機能しない理由

科学計算や計測データ処理において、数式を簡略化したり置き換えたりする際、従来の代数的等式（$A = B$ なら $A$ を $B$ に置き換えてよい）は 2 つの主要な失敗モードにより破綻します。

1. 出所（Provenance）の無視

   • 問題点: 同じ観測値が式の中で 2 回現れる場合、それは「1 つの隠れた真値」を共有しています。しかし、2 つの独立した観測値（たとえ同じ計測器・不確かさ範囲であっても）は、真値が一致するとは限りません。
   • 例: $x - x$ は、$x$ が単一の計測トークンを指すなら 0 に書き換えられますが、$x_1 - x_2$（2 つの独立した観測）を 0 に書き換えることは一般に正当化されません。従来の次元解析や区間算術は、この「トークンの同一性」を区別できません。

2. 定義域（Definedness）の無視

   • 問題点: 除算（割り算）は特異点（分母が 0 になる点）を導入します。代数的に等しい式でも、定義される範囲（ドメイン）が異なる場合があります。
   • 例: $x/x$ は $x \neq 0$ で 1 に等しいですが、定数 1 はどこでも定義されます。$1$を$x/x$ に置き換えることは特異点を導入することになり、安全ではありません。逆に、特異点を除去する書き換えは安全ですが、その逆は成り立ちません。また、共通の定義域では同じ関数であっても、特異点の構造が比較不可能な場合、双方向の置き換えは不可能になります。

これらの問題により、科学的な数式最適化においては、トークンの出所と定義域の両方を考慮した厳密な書き換え分類が必要です。

2. 手法：統一的な意味論フレームワーク

著者らは、トークンに敏感な区間意味論（Token-sensitive enclosure semantics）と、許容ドメイン（Admissible domain）を統合したフレームワークを構築しました。

2.1 構文と評価

• 式言語: 定数、計測値（トークン $t$、区間 $I$、次元 $d$ を持つ）、および四則演算からなる最小限の言語。
• トークン環境: 各トークンに有理数を割り当てる関数 $\sigma$。同じトークン $t$ が式に複数現れる場合、$\sigma(t)$ は同じ値を共有します。
• 保証された区間（Warranted Enclosure）: 式 $e$ に対して、すべてのトークン整合的な環境 $\sigma$ で得られる値の集合 $Encl(e)$。これは出所情報を反映します。

2.2 定義域の追跡

• WellDefined: 式 $e$ が環境 $\sigma$ で定義されるか（すべての除算の分母が 0 でないか）。
• 許容ドメイン（AdmDom）: トークン整合かつ WellDefined である環境の集合。
• 定義済み区間（Defined Enclosure）: 許容ドメイン内でのみ評価された値の集合 $DefinedEncl(e)$。

2.3 書き換え判定基準

3 つのレベルで書き換えを定義します。

1. 区間ベース（Enclosure-based）: 出所のみを考慮。$e \leadsto e'$ は $Encl(e') \subseteq Encl(e)$。
2. ドメイン認識型（Domain-aware）: 定義域を考慮。
   • DomainSafeRewrite ($e \leadsto_d e'$): 対象 $e'$ の許容ドメインがソース $e$ のそれを包含し、かつソースのドメイン内での値がソースの定義済み区間に含まれる。
   • DomainEqual: 共通の定義域内でのみ値が一致する（双方向の書き換えを保証しない）。
3. サポート相対型（Support-relative）: 特定の環境集合（サポート）に限定した許容性を定義し、局所的な正の分類（例：正の区間での自己除算）を統合します。

3. 主要な貢献と結果

3.1 正の分類ファミリー（Positive Classification Families）

以下の 3 つの典型的な操作について、どのような条件で書き換えが正当化されるかを分類しました。

• キャンセル（同トークン）: $Meas(t, I) - Meas(t, I) \iff 0$。トークンが共有されれば 0 になります。
• 背景減算: $(s + b) - b \iff s$。背景 $b$ が同じトークンであれば正当化されます。
• 正の区間での自己除算: $Meas(t, I)/Meas(t, I) \iff 1$。区間 $I$ が 0 を含まず、かつトークンが共有されれば 1 になります。
• 対照: トークンが異なったり、区間に 0 が含まれたりする場合、書き換えは「一方向のみ（One-way）」または「不可能」になります。

3.2 厳密な負の結果（Strict Negative Results）

• 一方向性の書き換え: 特異点を除去する書き換え（例：$x/x \to 1$）は安全ですが、逆（$1 \to x/x$）は特異点を導入するため安全ではありません。
• 非縮退（Non-collapse）: 共通の定義域で同じ値をとる 2 つの式（例：$x/x$ と $(x-1)/(x-1)$）は、定義域の包含関係が双方向に成り立たないため、互いに置き換えられません。
• 不十分性定理: トークン出所を消去した「出所無視」の比較では、定義域の違いだけでは区別できない書き換えクラスを区別できません。逆に、定義域のみを追跡しても、トークンの同一性を無視すれば区別できません。両方が必要不可欠です。

3.3 還元と回復定理

• 普遍許容部分: 除算による特異点が存在しない場合（または区間が 0 を含まない場合）、ドメイン認識型の判定は従来の区間ベースの判定に還元されます。
• 回復定理: 正の区間での自己除算や背景減算などの操作は、サポート相対的な文脈で「回復」され、統一的な理論の一部として扱われます。

3.4 形式化

• 約 2,700 行の Lean 4 コードで、143 の定理と 45 の定義が「sorry」なしで形式化されました。
• 有理数 $\mathbb{Q}$ を使用しており、すべての結果が決定可能で計算に友好です。

4. 意義と結論

本論文は、計測データを含む数式の書き換えにおいて、従来の「代数的等式」や「値の一致」だけでは不十分であることを実証しました。

• 理論的意義: 「出所（Provenance）」と「定義域（Definedness）」という 2 つの直交する軸が、書き換えの正当性を決定するために両方とも必須であることを示しました。どちらか一方を欠いた意味論では、安全な書き換え分類は不可能です。
• 実用的意義: 科学的な数式最適化やシンボリック計算システムを設計する際、単なる代数簡約ではなく、観測の依存関係（トークン）と定義域の制約を明示的に追跡する必要があることを示唆しています。
• 機械検証: 複雑なドメイン包含関係や非推移性（$A \to B, B \to C$ だが $A \to C$ ではない）などの直感に反する性質を、機械検証によって厳密に保証しました。

結論として、安全な書き換え体系を構築するには、値、出所、定義域のすべてを統合した、より高次な意味論的枠組みが必要であり、本論文はそのための基礎的な定理パッケージを提供しています。