💻 computer science

Cyclic Proofs in Hoare Logic and its Reverse

本論文は、不変条件や停止性測度を明示的に必要とする従来の公理的証明系に対し、ループの展開と循環推論の健全性条件を用いる循環証明系を、部分正しさ・完全正しさのホアール論理およびその双対である逆ホアール論理（誤り論理）の両方に適用し、それらの健全性と相対的完全性を示すものである。

原著者： James Brotherston, Quang Loc Le, Gauri Desai, Yukihiro Oda

公開日 2026-03-03

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

CC BY 4.0

原著者： James Brotherston, Quang Loc Le, Gauri Desai, Yukihiro Oda

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

1. 物語の舞台：プログラムの「正しさ」と「間違い」

まず、この論文が扱っているのは、コンピュータプログラムが「意図した通りに動くか（正しさ）」、あるいは「意図した通りにバグ（間違い）が起きるか」を証明する話です。

従来の方法（ホアール論理）：
「このプログラムは、絶対にバグを起こさないよ」と証明したいとき、昔から使われている方法は**「ループの壁」**を作ることです。
- 例え: 迷路を脱出する際、「もしこの壁にぶつかったら、必ず出口へ向かう」という**「魔法の壁（不変条件）」**を自分で見つけて、それを証明する必要があります。
- 問題点: この「魔法の壁」を見つけるのは非常に難しく、自動化するのが大変でした。
この論文の新しい方法（循環証明）：
「魔法の壁」を自分で見つける代わりに、**「迷路をぐるぐる回りながら、いつか必ず出口にたどり着く（あるいはバグにぶつかる）」**という証明方法を使います。
- 仕組み: 証明の途中で、すでに証明した部分に戻って（ループして）、無限に続く道筋を描きます。そして、「この無限の道筋は、実は矛盾している（つまり、バグは存在しない）」と示すことで正しさを証明します。

2. 2 つの視点：「正しさ」と「間違い」の鏡像

この論文の最大の特徴は、**「正しさ」と「間違い（バグ）」**を、まるで鏡に映したように対称的に扱っている点です。

A. 正しさを証明する（ホアール論理）

目標: 「このプログラムは、必ず正しい結果を出す」こと。
ループの証明:
- 部分正しさ: 「もしプログラムが止まれば、正しい結果になるはず」という証明。
  - イメージ: 迷路を歩き続ける限り、いつか出口にたどり着く（または無限に歩き続けるが、バグには出会わない）。
- 完全正しさ: 「このプログラムは、必ず止まって正しい結果を出す」こと。
  - イメージ: 迷路を歩くたびに、**「エネルギー（体力）」**が減っていくことを証明する。エネルギーが尽きれば必ず止まるので、無限に歩き続けることはあり得ない。

B. 間違いを証明する（リバース・ホアール論理）

目標: 「このプログラムは、必ず特定のバグ（または状態）に到達する」こと。
- 例: 「このコードを実行すれば、必ず『エラー画面』が表示される」ということを証明したい場合です（バグ発見の自動化に役立ちます）。
ループの証明:
- ここでも「正しさ」と同じように、**「魔法の壁」を見つける代わりに、「無限に回り続ける道筋」**を描きます。
- イメージ: 「この迷路を歩けば、必ず特定の罠（バグ）に落ちる」ということを、無限に続く道筋の中で示します。

3. この研究のすごいところ：「鏡の対称性」

研究者たちは、この 2 つの世界（正しさと間違い）が、実は同じルールで動いていることに気づきました。

正しさを証明するルールと間違いを証明するルールは、まるで鏡像（ミラーイメージ）のように似ています。
従来の方法では、正しさを証明するときは「壁」が必要で、間違いを証明するときはまた別の「壁」が必要でした。
しかし、この新しい**「循環証明（Cyclic Proofs）」という方法を使えば、「壁」を探す必要がなくなります。**
- 代わりに、**「無限に続く道筋の中に、矛盾がないか（正しさの場合）あるいは必ずバグがあるか（間違いの場合）」**をチェックするだけで済みます。

【簡単な比喩】

昔の方法: 迷路の出口を見つけるために、地図を自分で描き直して「ここが壁だ！」と指差す必要があった。
新しい方法: 迷路を歩きながら、「もしここから先が無限に続くなら、それはバグだ（あるいは正しくない）」と、道筋そのものの形だけで判断する。

4. なぜこれが重要なのか？

自動化がしやすくなる:
「魔法の壁（不変条件）」を人間が考えなくて良くなるので、コンピュータが自動的に証明を見つけやすくなります。
バグ発見の強化:
「間違いを証明する（バグがあることを示す）」という考え方が、正しさを証明するのと同じくらい体系的に扱えるようになりました。これにより、自動でバグを見つけるツールがもっと賢くなる可能性があります。
統一された視点:
「正しさ」と「間違い」という一見相反する 2 つの概念が、実は同じ数学的なルール（循環証明）で説明できることがわかりました。これは、プログラムの理論を整理する上で非常に美しい発見です。

まとめ

この論文は、「プログラムの正しさを証明する際、難しい『壁』を探す代わりに、無限に続く『道』を描いて証明しよう」というアイデアを、「正しさ」と「バグの発見」の両方に適用し、それらが同じルールで動いていることを示したという研究です。

まるで、迷路を解くために「出口への地図」を描くのではなく、「無限に続く迷路ならそれは間違いだ」という**「道そのものの性質」**で判断する、新しいアプローチの提案と言えます。

論文「Cyclic Proofs in Hoare Logic and its Reverse」の技術的概要

この論文は、プログラムの正しさ（Hoare 論理）と誤り・到達可能性（Reverse Hoare 論理／Incorrectness 論理）を扱う論理体系において、公理的証明系と**循環証明系（Cyclic Proofs）**の関係を統一的に定式化し、両者の健全性（Soundness）と相対的完全性（Relative Completeness）を証明したものです。

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

1. 問題設定 (Problem)

プログラムの検証において、ループ構造（while ループ）の証明は中心的な課題です。

公理的証明系（従来のアプローチ）:
- 部分正しさ（Partial Correctness）: ループ不変式（Loop Invariant）の発見が必要です。
- 完全正しさ（Total Correctness）: ループ不変式に加え、ループの終了を保証する**整礎な停止尺度（Well-founded Termination Measure）**の発見も必要です。
- 課題: これらの不変式や停止尺度を自動的に見つけることは困難であり、自動化された証明探索の大きな障壁となっています。
Reverse Hoare 論理（逆 Hoare 論理）:
- プログラムが「ある状態から出発して、特定の到達状態に到達する（あるいはバグが発生する）」ことを証明する論理です（Incorrectness 論理とも呼ばれる）。
- これまでの研究では、公理的証明系は存在するものの、循環証明の枠組みでの定式化は十分に行われていませんでした。

本研究の目的:
Hoare 論理（部分・完全）と Reverse Hoare 論理（部分・完全）の 4 つの体系に対して、循環証明系を構築し、それらが公理的証明系と等価であることを示すこと、および両者の対称性（Dualty）を明らかにすることです。

2. 手法とアプローチ (Methodology)

著者は、単純な while プログラム言語を基盤とし、以下のステップで研究を進めました。

A. 証明系の定式化

公理的証明系:
- 従来の Hoare 論理（PHL, THL）と Reverse Hoare 論理（PRHL, TRHL）の公理的証明規則を定義しました。
- ループ規則において、不変式や停止尺度を明示的に要求する規則（Inv, Inv-Total など）を使用します。
循環証明系（Cyclic Proof Systems）:
- 証明木を有限の木構造とし、葉ノードを内部ノードへ「バックリンク（Backlink）」で結ぶことで、無限の証明木（Pre-proof）を表現します。
- ループ処理: ループ不変式の明示的な発見を不要とし、ループを 1 回展開する規則（CInv, CRInv2 など）のみを使用します。
- 継続スタイル（Continuation Style）: 証明規則を {P} C {Q} ではなく {P} C; C' {Q} のように、残りの命令 $C'$ を含めた形で記述し、証明の合成を容易にしています。

B. 循環証明の健全性条件（Global Soundness Conditions）

循環証明が正当であるためには、証明木内の無限パスが特定の条件を満たす必要があります。

部分正しさ（PHL, PRHL）:
- 無限パス上で、**記号的実行規則（Symbolic Execution Rules）**が無限回適用されることを要求します。
- 意味: 反例（プログラムが正しくない実行）が存在すると仮定すると、それは有限の長さで終わるはずですが、記号的実行が無限に続くため、反例は実際には無限実行（発散）となり矛盾します。これは**余帰納的（Coinductive）**な性質です。
完全正しさ（THL, TRHL）:
- 無限パス上で、事前条件に含まれる**整礎な値（停止尺度など）の無限に減少する列（Trace）**が存在することを要求します。
- 意味: 反例が存在すると仮定すると、それは有限の停止を持つはずですが、停止尺度が無限に減少するため、それは無限ループ（発散）となり矛盾します。これは**帰納的（Inductive）**な性質です。

C. 翻訳と完全性の証明

公理的証明から循環証明への翻訳:
- 任意の公理的証明を、バックリンクを持つ循環証明に変換するアルゴリズムを構築しました。
- ループ規則（Inv や Inv-Total）に対応する部分で、証明木の根をループの展開規則（CInv など）の結論へバックリンクさせることで、循環構造を生成します。
健全性の直接証明:
- 循環証明が定義された意味論的妥当性を満たすことを、無限パスの性質（無限実行または無限減少列）を用いて直接証明しました。

3. 主要な貢献と結果 (Key Contributions & Results)

1. 4 つの論理体系の統一的な循環証明定式化

Hoare 論理（部分・完全）と Reverse Hoare 論理（部分・完全）の 4 つの組み合わせすべてに対して、同じ証明規則（ループ展開規則など）を共有しつつ、健全性条件のみを切り替えることで循環証明系を構築しました。

PHL (部分 Hoare) と PRHL (部分 Reverse Hoare): 健全性条件は類似しており、余帰帰納的（Coinductive）な性質を持ちます。
THL (完全 Hoare) と TRHL (完全 Reverse Hoare): 健全性条件は類似しており、帰納的（Inductive）な性質を持ちます。

2. 健全性（Soundness）と相対的完全性（Relative Completeness）の証明

健全性: 循環証明系で導出可能な triple は、すべて意味論的に妥当であることを証明しました。
相対的完全性: 公理的証明系で証明可能な triple は、すべて循環証明系でも証明可能であることを、明示的な翻訳アルゴリズムによって示しました。
- 注: 部分 Reverse Hoare 論理（PRHL）の公理的証明系の完全性については、完全な証明は未完了ですが、循環証明系への翻訳は成功しています。

3. 双対性（Duality）の明確化

部分 Reverse Hoare 論理（PRHL）と完全 Hoare 論理（THL）、および完全 Reverse Hoare 論理（TRHL）と部分 Hoare 論理（PHL）が、意味論的・証明論的に双対であることを示しました。
特に、PRHL は「完全正しさの双対」として自然に導かれる新しい論理体系として位置づけられました。

4. 新規な論理体系の提示

PRHL（部分 Reverse Hoare 論理）: これまであまり注目されていなかった、あるいは未定義だった「部分到達可能性」を扱う論理体系を提案し、その循環証明系を構築しました。

4. 意義と将来展望 (Significance & Future Work)

意義

理論的統合: Hoare 論理と Incorrectness 論理（バグ検出）を、循環証明という単一の枠組みで統一的に扱えることを示しました。これにより、正しさの証明と誤りの証明の間の深い対称性が可視化されました。
自動化への寄与: 循環証明は、ループ不変式や停止尺度を人間が手動で設計する必要を減らすため、定理証明支援系（例：Cyclist）や自動検証ツールの実装において、より効率的な証明探索を可能にする可能性があります。
証明の簡素化: 公理的証明における複雑な不変式の発見プロセスを、証明木の循環構造（バックリンク）とグローバルな条件に置き換えることで、証明の構造を単純化しました。

将来の展望

実装: 提案された循環証明系を、Cyclist などの既存の定理証明支援系に実装し、実際のプログラム検証への適用性を検証する。
Incorrectness 論理の拡張: 既存の Incorrectness 論理のシステムに、循環証明の原理を統合し、より強力なバグ検出手法を開発する。
複雑な言語への拡張: 手続き呼び出しや関数、並行処理を含むより複雑なプログラミング言語への適用。

まとめ

この論文は、Hoare 論理とその双対である Reverse Hoare 論理を、循環証明の枠組みで再構築した画期的な研究です。公理的証明における「不変式発見」という困難な課題を、証明木の循環構造とグローバルな健全性条件に置き換えることで、部分正しさと完全正しさ、そして正しさと誤りの証明を統一的に扱える体系を確立しました。これは、形式検証の理論的基盤を強化し、将来的な自動化ツールの発展に重要な指針を与えるものです。