ホーア論理との出会い

7332 ワード
論理学 Coq Coq テキストリンク

ホーア論理という「手続き型プログラミング言語の挙動」を形式化する手法について勉強しました。主に論理学的なバックグラウンドを持つ人に説明することを想定して、私の理解を整理します。

参考文献は『Software Foundations Vol.2』という無料・オンラインの大学院生向けのテキストです。しかし、本稿では私なりの解釈がそこそこはいっていることをお断りしておきます

01. 全体像

証明論or意味論: ホーア論理は論理学の一種なので（より正確にいうと論理学でいうところの理論の一種なので）証明論的/公理的なアプローチと、意味論的/モデル論的なアプローチという 二つの異なる立場がありえます。完全性定理が成立するので どちらの立場をとってもよいのですが、通常は意味論的な立場をとります。その理由はモデルである「プログラミング言語の挙動」が十分なじみ深い存在であるからかもしれません。どちらの立場に立つかはテクニカルな問題にすぎず、実践上の違いはほぼありません。例えばCoq上でホーア論理を展開する時は 意味論的な立場をとることが多いですが、「公理的な立場において公理とみなされる論理式」の正しさを確認して道具立てとします（＝論理的帰結関係に関する規則とみなして証明します）。つまり 意味論的な立場をとっても公理は正しい道具立てであり、積極的に使うことができますし、使うことが必須といっても過言でありません。

階層化された分析手法: 空気が分子で出来ていることを知らなくても熱力学を展開できるように、世の中の事象の多くは階層化した分析/reasoning で説明できます。これは ホーア論理関連の話題にもあてはまります。前述のように 意味論的/モデル論的な立場を取るので、粒度の一番細かい分析で全てを説明することは面倒ではありますが可能です。つまり プログラムを state =[cmd]=> state' で図示されるような状態変換装置のように捉えることで、分析対象であるプログラムの振舞い/behaivior に注目した分析手法に還元できます。一方、もう少し粒度を大きくした分析も可能です。つまりプログラムを {P} cmd {Q} で図示されるような アサーション変換装置 のように捉えることで、プログラムの検証/verification という概念に到達します。この粒度での分析がホーア論理の主戦場です。つまり、ホーアトリプルの定義に立ち返ることなく（＝粒度を細かくすることなく）検証が行えるのです。アサーション間の含意関係 {P}->>{Q}やホーア帰結関係/hoare consequences という道具立てを使うことで、プログラムの各ステップを規約で装飾/decorate するという形で分析・検証が可能になります。

リレーショナルな評価: プログラムを 状態変換装置として見るにせよ、アサーション変換装置としてみるにせよ、そこには入力と出力があるので、何らかの変換手続きを検討・実装したくなります。しかしながら、ここは一旦立ち止まるところです。別のアプローチ、すなわちリレーショナルな方法があり、形式証明ではそちらの道を歩みます。つまり 状態 st を プログラム c にいれたら st' になるような関数 f を検討・実装するのではなく、R st st' c なる三項関係 R を構成するのです。これは集合論や数理論理学における関数とそのグラフの関係に似ています。例えば平方する関数 square を実装して y = square x とするのも一つの方法ですが、「・と・は平方の関係にある」という二項関係つまりその外延が (0,0),(1,1),(2,4)... となるグラフを構成してもよいのと同じことです。このように関数ではなく関係として捉えるのが重要です。この考えの下では、状態変換は、三項関係であるコマンド評価関係 ? =[?]=> ? の成立として捉えるべきですし、アサーション変換は三項関係であるホーアトリプル関係 {{?}} ? {{?}} の成立として捉えます（注: ? のところに要素がはいります)

small step意味論: 上述したような評価に関するリレーショナルな方法をとことん突き詰めたモデル・意味論(small step意味論）も検討できます。このモデルのよいところは、評価関係をより粒度を細かく分析できることです。並列計算などでは、プログラム・入力状態・出力状態　以外のモノ（例：プログラム実行中における他ノードの計算状態）が表舞台に立つことがあり、そのような手続き型プログラムの分析・検証にはより詳細なモデルが必要になるというわけです。問題意識さえ持てれば、そのモデルを構築することは煩雑ではありますが、特に難しいところはありません。small stepな操作論的意味論は ラムダ計算や型理論において必須の道具立てとなりますが、とりあえずこれ以上踏み込みません（以降は big-stepな意味論で話をします）。

02. ホーア理論のモデル

意味論的な立場を取るので、各種存在物や各種関数記号・関係記号の解釈を明示しましょう。ホーア論理は構成主義的でmany-sortedな論理上で展開され、論理語の解釈はBHK解釈（＝カリーハワード対応でよく使う意味論）になります。

式/expression: aexp または bexp という型をもつ存在物です。前者の例は 5, 3+2, X+3, X+2*Y などで後者の例は X<=1, X=2+Y, ~X+Y+Z<=12 などです。表層的にはただの記号列ですが、Inductiveな構成法に従います。なお、前者は自然数、後者はブール値 と評価関係になりうる（≒と評価されうる）という違いがあります。式の型の種別は増やしてもよいです。

コマンド/command, プログラム/program: cmdという型を持つ存在物です。典型的には「代入/assignment」「継続/sequence」「条件分岐/if」「ループ/while」などの構成子を持つInductiveな構成法に従います。例として X::=1, Y::=X*X, IF X=0 THEN Y::=1 ELSE Y::= 0 FI, X::=1;; Y::=X+1, WHILE ~X=0 DO X::=X-1 END などです。例をみれば分かるように、ほとんどの構成子はひとつまたは複数の aexp や bexp や cmd でインデックスされます。なお、コマンドとプログラムの違いはありません。

状態/state: stateという型を持つ存在物です。マシン状態とも言われます。変数値を覚えておく入れ物、例えば {X:10, Y:7} 等のイメージで持てば当面はよいです。total mapとして実装することが多く、その場合デフォルト値は0にします。

評価/evaluation: 上述の存在物はそれぞれの対応物と評価関係になりえます。aexpは（ある状態の下で）自然数に、bexpは（ある状態の下で）ブール値に、stateは（あるコマンドの下で）べつのstateに、という具合です。small stepでない(natural semantics/big step)な意味論では aexp, bexp は評価関数として実装され、stateは評価関係として実装されます。後者は st =[c]=> st' という表記法で表されます。状態がコマンドによって変化する様子が見た目にも明らかです。プログラミング言語の振る舞いは この評価関数/関係をどう構成するかによって完全に特徴づけられます。

アサーション/assertion: 全てのstateを集めた集合の部分集合です。直観的には「細かくは指定しないが特定の条件が成り立っている状態の集まり」です。たとえば「X=1だがその他の変数値はなんでもよい」時には、非形式的には {{X=1}} と書き、Coq上で表現するときは {{fun st => st X = 1}} のように書きます。つまり単一の状態ではなく 特定の条件を満たした複数の状態を「束ねて」議論するための道具立てです。

ホーアトリプル/hoare triple: アサーションが（あるコマンドのもとで）別のアサーションを含意することがあります。直観的には「アサーションPの任意の要素である状態をコマンドに通したときの状態は必ずアサーションQに含まれる」ような場合です。ごく単純な例では {{X=1}} は X::=X+1 の下で {{X=2}}になります。このような状況を表す 二つのアサーションと一つのコマンドの3項関係をホーアトリプルといい、{{P}} c {{Q}}などの表記をします。ホーアトリプル関係が成立するかどうかは、プログラミング言語の振舞い（つまり評価関数・評価関係の規則）から決まります。よって、ホーアトリプル関係が成立するための特別な公理や構成法があるわけではありません。これは意味論的な立場すなわちこれまで見てきたようなモデルを想定しているからです。証明論的な立場では公理を作ります。意味論的にはその公理の正しさを証明し、道具立てとします。

03. ホーア論理の実践

「ならば」っぽい概念を整理: (P:Prop)->(Q:Prop) は含意です。BHK解釈ではPの証拠をQの証拠に変換する関数です。「Pが成立するならばQが成立する」と読めます。aeval (st:state) (a:exp) = (n:nat)は式の評価関数に関するPropです。「状態stの時aならばnに評価される」と読めます。bevalも同様です。st =[c]=>st' はコマンドの評価関係に関するPropであり、「入力状態がstでコマンドcを実行するならばst'になる」と読めます。{{P}}->>{{Q}}はアサーションにおける含意であり「Pな状況ならばQの状況になっている事が言える」と読めます。{{P}}c{{Q}}はホーアトリプル関係が成立していることを主張する言明で「Pな入力状況でコマンドcを実行するならばQという出力状況になる」と読めます。

ホーア帰結関係: ホーア論理の公理のうち重要な公理/証明規則は {{P}}->>{{Q}}と{{Q}}c{{R}} から {{P}}c{{R}}を帰結してもよいということです。これは上述のように両者をならばと読む時、自然に思えます「Pの状況ならQな状況が成り立ち、QがRに変換されるのが確かなら、Pの状況においてプログラム実行するとRの状況は成立しているだろう」。同様にアサーションの含意を後置する規則もあります。すなわち {{P}}c{{Q}}と{{Q}}->>{{R}}から{{P}}c{{R}}を帰結してもよいのです。
この二つの（正しいと証明された）ルールは、ホーア論理の公理適用の前段階の調整として非常に役立ちます。

装飾されたプログラム: プログラムはコマンドの合成して作られており、合成の方法は継続・条件分岐・ループくらいのものです（参考：構造化定理）なので合成の各部品すなわち、一般的なプログラミング用語におけるステップから構成されているわけで、各ステップのcmdをホーアトリプルで囲ってホーア論理の公理適用が明確な形に装飾/decorateすることで、プログラムの検証はほとんど自明なものになります。たとえば {P}c1;c2;c3{Q}というプログラムを実装したとしましょう。つまり「状況Pを状況Qにマップするプログラム」を実装し、その正しさを検証してみましょう。前述のホーア帰結関係を使って

{P}->>{P1}c1{P1'}->>{P2}c2{P2'}->>{P3}c3{P3'}->>{Q}

が装飾されたプログラムです。ホーア帰結関係が役立つところです。{Pi}ci{Pi'}というホーアトリプルは、ホーア理論の公理そのもの（もしくはその例化）にすることで、証明不要になります。なので検証するべきはホーアトリプル同士のつなぎ目、の「アサーションの含意関係」のみを証明すればよくなり、プログラムの検証をより単純な問題に還元できます。どのようなアサーションを選ぶかが、プログラマの創造性を発揮するところになります

装飾されたプログラムの作成法とループ不変条件: プログラマの創造性はプログラム全体を囲うアサーションの同定（≒仕様の策定）と、そこから各ステップにアサーションを埋め込む作業です。前者はビジネスロジックからほぼ自動的にきまりますが、後者はあたまを悩ませるところです。とはいえ、機械的にできる部分がほとんどで、本当に頭を悩ませるのはWHILEループが絡むときのアサーションの同定です。このあたりは個別的な話になるので、SoftwareFoundationsなどに多くの問題があるのでやってみると面白いです（分からなくても少し先にいくとほぼ解答に近いのが載っています）。

04. 最後に

Software Foundations のVol.2あたりからCoqの勉強・Coqの世界観というよりも、ソフトウェア・プログラミング言語そのものに関する性質や洞察を行うことが増えてきて楽しくなってきました（とはいえ、私個人の興味の方向とは少し違うのですが・・・）

Vol 1.と比べてはるかに難しくなっているのを感じます。Vol2.まではなんとか課題を解き切りたいと思います（数カ月単位の時間がかかりそうです）