Anti-Unification Completeness Analysis in PVS

想像してみてください。あなたの手元には、全く異なる2つのレゴのお城があります。一つは小さくて単純な塔、もう一つは秘密の通路を備えた巨大で複雑な要塞です。次に、両方の城の「本質」を捉える「マスター・ブループリント（設計図）」を作りたいと考えているとします。あなたは、両者が共有する部分（例えば「ドアがある」「屋根がある」など）を見つけ出し、独特で紛らわしい部分は一般的なプレースホルダー（例えば「ある色のブロック」など）へと変換したいと考えています。この、共通点を見つけ出しながら差異を隠すプロセスが、「アンチ・ユニフィケーション（反単一化）」と呼ばれるものです。

何十年もの間、コンピュータ科学者たちは、この設計図を作るためのレシピ（アルゴリズム）を使用して、バグを修正したり、コピーされたコードを見つけ出したり、あるいは低速なソフトウェアを高速な並列ソフトウェアへと変換したりしてきました。しかし、そこには落とし穴がありました。レシピ（アルゴリズム）を使って設計図を作る方法は持っていたものの、あらゆる可能な「城のペア」に対して、そのレシピが常に完璧に機能するという数学的に堅牢な保証までは持っていなかったのです。私たちは、それがクラッシュしないこと（「健全性」があること）は知っていましたが、それが毎回必ず「最善の」設計図を見つけ出すこと（「完全性」があること）までは証明できていませんでした。

この論文は、デジタル証明チェッカーであるPVSを用いて、ついにその欠けていた保証を構築した研究チームの物語です。

「解決済み」のピースというパズル

なぜこれがこれほど困難だったのかを理解するには、アルゴリズムがどのように機能するかを見る必要があります。アルゴリズムは、2つの城をパーツごとに分解していきます。

• 簡単な部分： もし、2つのパーツが同一のレンガであると判断した場合、アルゴリズムは「了解！」と言って、そのまま次に進みます。
• トリッキーな部分： もし、2つのパーツが異なるレンガ（例えば、赤と青）であった場合、通常の照合ゲームのように諦めることはしません。代わりに、「ああ、これらは違うものだ！この違いを記憶しておき、他の場所でも同様の赤対青の不一致がないか探し続けよう」と考えます。

通常の照合ゲーム（「ユニフィケーション」と呼ばれます）では、違いを見つけることは即座に敗北を意味します。しかし、アンチ・ユニフィケーションにおいては、違いを見つけることこそが「目的」なのです。アルゴリズムは、見つけたすべての差異を記録する「日記」を付け続けなければなりません。

研究者たちは、アルゴリズムの「簡単な部分」を証明することが、驚くほど困難であることを発見しました。実際、アルゴリズムが正しいことを証明するために費やされた労力の**91.10%**は、まさに2つの特定のケース、すなわち「解決済み」の問題（アルゴリズムが差異を検知する場合）と「構文的（シンタクティック）」な問題（パーツが同一である場合）の処理に費やされました。これらは単純に聞こえますが、アルゴリズムが混乱することなくこれらの差異を正しく記録できているかを証明するには、膨大な量の厳密な検証が必要でした。

アルゴリズムの「歴史書」

この論文における主要なブレイクスルーは、アルゴリズムが最善の設計図を見つけることを証明するためには、現在のステップだけを見るのではなく、計算の全履歴を見なければならないと気づいたことです。

著者らは、アルゴリズムの「メモリ（記憶）」に関する新しい考え方を導入しました。彼らは「全般化子（Total Generalizer）」、つまり以下の要素を考慮したマスター・ブループリントを定義しました。

1. まだチェック待ちの状態にあるパーツ。
2. すでにチェックされ、「異なる」とマークされたパーツ。
3. アルゴリズムが進むにつれて構築されている「置換（substitution）」（ルールのリスト）。

彼らはいくつかの「不変性（invariance properties）」を証明しました。これらは、「アルゴリズムが何ステップ実行されようとも、これまでに発見された差異の総リストが消えたり、その意味が変わったりすることはない」というルールのようなものです。彼らは、アルゴリズムが大きな問題を小さなサブ問題へと分解していく過程においても、元の問題の「物語」は、まるでジグソーパズルのピースをバラバラにして混ぜ回しても、元の絵が変わらないように、そのまま維持されることを示しました。

「制限された」設計図

ここには巧妙な仕掛けがあります。証明を成立させるために、著者らは**「制限された全般化子（Restricted Total Generalizer）」**という特別な種類の設計図を考案する必要がありました。

想像してみてください。あなたがレシピを書こうとしているとします。もし、すでにキッチンにある材料（アルゴリズムが現在使用している変数）を使ってしまうと、レシピを書いている最中に、意図せずレシピ自体を変えてしまうかもしれません。そこで著者らは、「証明には、新鮮で未使用の材料（変数）だけを使おう」と決めました。彼らは、もし「新鮮な」材料を用いた設計図を見つけることができれば、それを通常の設計図へと常に翻訳できることを証明しました。

設計図をこれらの「新鮮な」材料に限定することで、彼らは定理20を証明することができました。すなわち、アルゴリズムの最終的な結果は、考えうる他のいかなる設計図よりも、少なくとも同等に具体的であるということです。言い換えれば、アルゴリズムはより良い解を見逃すことはありません。

これが意味すること（および意味しないこと）

この論文は、構文的アンチ・ユニフィケーションのためのルールベースのアルゴリズムが**完全（complete）**であることを（単なる示唆ではなく）証明しています。これは、このアルゴリズムが、任意の2つの項に対して、最小の一般化子（最も精密な共通の設計図）を必ず見つけ出すという数学的な保証があることを意味します。

しかし、論文内では、まだ達成されていないことについても非常に慎重に記述されています。

• 本論文は、今すぐ実行可能な最終的な「マシンチェック済みの実行可能コード」を提供しているわけではありません。著者らは、新しい定義と補題の定式化は「進行中の作業（work in progress）」であると述べています。
• 本論文は、すべての種類の数学（交換法則や結合法則を含むものなど）に対するアンチ・ユニフィケーションを解決したと主張しているわけではありません。あくまで「構文的（シンタクティック）」なアンチ・ユニフィケーション（標準的なもの）に焦点を当てています。
• 本論文は、アルゴリズムが速度の面で高速である、あるいは効率的であると主張しているわけではありません。あくまで、その「論理」が正しく、完全であることを証明しています。

結論

この論文は、コンピュータアルゴリズムの厳密かつ段階的な解剖図です。著者らは単に「動く」と言ったのではありません。彼らは、特にアルゴリズムが差異を検知するという地味ながらも極めて重要なステップにおいて、あらゆるステップを検証する「論理のデジタル要塞」を築き上げました。計算の完璧な「歴史書」を保持し、解決策に対する巧妙な「制限された」思考を用いることで、アルゴリズムが常に正しい答えを見つけ出すことを保証できることを示したのです。

今、数学的な証明が完了したことで、次のステップへの扉が開かれました。それは「認定済み実行可能コード（certified executable code）」の抽出です。これにより、将将来、コードや化学化合物の共通パターンを見つける際に決して間違いを犯さないことが数学によって保証されたソフトウェアへと、このアルゴリズムを変換できるようになるかもしれません。しかし、現時点での勝利は、その証明自体にあります。なぜそれが機能するのかという「謎」が、ついに解明されたのです。