この記事で導入した概念を使ってエクスペクテーションのモデルを構成するのは次回（続き）にします。
次回（続き）では、条件と実行文をあまり区別しない方法を紹介します。エクスペクテーションの定式化では、条件と実行文を区別しません。
と書いたのですが、先に進む前に、前回の補足説明とか言い残した事とかを書いておきます。階段で上の階に上がる途中の踊り場みたいなもの、ということで「踊り場・編」。
内容：
全体：
前回の復習
前回導入した道具立てをザッと復習しておきます。
非決定性写像の圏NDMapを舞台とします。ただし、この圏の対象（集合）と射（非決定性写像）だけではなくて、各対象ごとにブール代数Ω(S)が付随しているとします*1。この圏の対象Sが状態空間、射 S→T がプログラムの実行、ブール代数 Ω(S) が論理的条件のモデルになります。
射の集まりであるホムセットNDMap(S, T)には足し算（非決定性の選択）が定義されておリ、Ω(S)によるプレガード／Ω(T)によるポストガードをそれぞれ左スカラー乗法、右スカラー乗法として、NDMap(S, T)は“左Ω(S)-右Ω(T)-加群”*2の構造を持ちます。p∈Ω(S)、f:S→T、q∈Ω(q) に対して、p・f・q は、実行に先立ち条件 p で検査して、状態遷移 f を実行し、実行後に条件 q で検査するような射を表します。
特に、S = T のときは、エンドォセット NDMap(S, S) は、Ω(S)-両側加群です。さらに、射の結合を掛け算として、NDMap(S, S) にはベキ等半環の構造が入ります。つまりNDMap(S, S)は、可換半環Ω(S)上の両側多元環（両側代数*3）となります。
2006年に書いた次の記事は、今説明したような代数的な構造を利用した算術的計算（calculation）の事例です。
「データ型やプログラムを計算する」の最後にほうに、関連する他の記事への参照もあります。
理解しにくいところ、誤解しやすいところ
理論的には、非決定性写像は圧倒的に便利なんですが、非決定性写像って概念はわかりにくいと思います。次の記事を眺めてみてください。
- 状態遷移機械と非決定性遷移 - 檜山正幸のキマイラ飼育記 (はてなBlog)
- コインとサイコロで非決定性プログラミングをお手軽に実験してみるよ - 檜山正幸のキマイラ飼育記 (はてなBlog)
- 非決定性プログラミングだって絵を描いてみれば一目瞭然 - 檜山正幸のキマイラ飼育記 (はてなBlog)
非決定性の写像fの点sにおける値が空集合のとき、fはsで未定義とみなします。これは、そこでプログラムが止まってしまう（実際は無限ループしてるかもしれません）、あるいは実行時例外が発生すると解釈すればいいでしょう。無限ループと例外は全然違うようですが、神様から見れば同じです。次の記事が多少は参考になるかもしれません。
ホーア論理を扱っていると、「プログラム自体」と「プログラムに対する判断」を誤解して混同することがしばしばあります。圏の言葉で言うと、「圏の射」と「圏の射に関する等式や不等式」を混同しちゃうのです。「全然別物だから区別できるだろう」と思うかもしれませんが、けっこう間違います。僕も間違ったことが何度もあります。
ホーア式 p{f}q は、プログラムfに対する判断・主張の表現です。その判断・主張は、だいたいは次のように書けます。
if (p) {
f; // ここで状態遷移が起きる
return q;
} else {
return true;
}
一方、if-then-else文は p・f + ¬p・g の形に書けます。そのため、ホーア式 p{f}q を、圏のなかにエンコードすると「p・f + ¬p・I となるのではないか」とか思ってしまいます。ホーア式（ホーアトリプル）のエンコードは p・f ⊆ f・q とか p・f・q = p・f であって、p・f + ¬p・I は関係ありません。そもそも p・f + ¬p・I は“プログラム＝射”を表すのであって、判断・主張になっていません。
最小なホーア論理
ホーア論理は、演繹系（証明系）です。前回は、モデル（意味論）の側でホーア式の解釈をしてしまいましたが、本来は構文としての論理式やプログラム文があって、それの解釈（値割り当て）の結果として条件や射が現れます。ここでは、演繹系としてのホーア論理のミニマムを紹介します。
p{f}q という形のホーア式があると、元来 p, q は論理式、f は何らかのプログラミング言語の実行文です。p{f}q は構文的な対象、つまり単なる記号的な図形として与えられるのです。ただ、人間はすぐに意味を与えたがるので、記号を記号のままにはしておけず、論理式を条件（状態空間上で定義された二値ブール値関数）、実行文を状態遷移と同一視（あるいは混同）する傾向があります。
今しばらくは、p{f}q を単に記号的図形だと思い、記号的な図形の組み合わせから、別な記号的な図形を生み出すルールを考えます。そのような、図形の取り扱いと操作に関するルールがホーア論理の推論規則です。標準的なホーア論理では、代入文、if文、while文などに関する推論規則がありますが、ここでは、「空文の公理」と「順次（逐次）実行の推論規則」だけにします。
●空文の公理
------
p{}p
●順次実行の推論規則
p{f}q q{g}r
--------------
p{f;g}q
論理式に含意記号「⊃」が（常識的な意味で）使えるときは、次の規則も採用します*4。
●含意 事前条件
p'⊃p p{f}q
---------------
p'{f}q
●含意 事後件条
p{f}q q⊃q'
---------------
p{f}q'
p'⊃p のような論理式を導くには、ホーア論理の背後にある論理（例えば古典論理）を使うことになります。つまり、ベースになる論理があって、そこにホーア式とそれに関する公理・推論規則を入れて拡張した論理体系がホーア論理（のインスタンス）です。今回は、「空文の公理」と「順次実行の推論規則」だけを付け加えた最小のホーア論理を導入しました。
プログラムの正しさとは
ホーア式 p{f}q が「成立する」とはどういうことか考えてみます。「成立する」のひとつの解釈は次です。
- 演繹系としてのホーア論理のなかで、ホーア式 p{f}q が証明できる。
実際には、プログラミング言語／ターゲットシステムに固有の公理／推論規則を付け加えるでしょうが； 証明できるとは、公理から出発して許された推論規則の連鎖により目的のホーア式が得られる、ということです。ホーア式 p{f}q が証明できることを |- p{f}q と書きます。
「成立する」のもうひとつの解釈は、適当なモデルに関して妥当であることです。モデルは、「領域と構造」と「記号の解釈」からなります。前回述べたことは、実はホーア式のモデルについてなのです。前回の話では、「領域と構造」として、「非決定性写像の圏＋ブール代数」を採用して、「記号の解釈」はイイカゲンで済ませたのでした。
プログラムの正しさの記述をホーア式の集合だと考えましょう。すると、プログラムが正しいと主張するためには、当該記述に含まれるすべてのホーア式が「成立する」必要があります。ホーア論理は健全なので、「|- p{f}q ならば、任意のモデルMで、M |= p{f}q」となることは保証されます。つまり、すべてのホーア式を証明し尽くせば、プログラムが正しいと主張してよいことになります。
ですが、現実的には「すべてのホーア式を証明し尽くす」のは困難です。代替案としては、ホーア論理の完全性を利用して、「すべてのホーア式を、すべてのモデルにおいて妥当性検証をする」方法があります。これもたいてい無理ですね。うまくモデルを見つけると、すべてのモデルの代わりに使えることがありますが、うまいモデルを見つけるのがこれまた難しい（特定状況では簡単になりえますが）。
そんな事情で、現実的には、結局プログラムの正しさを主張することはできません。で、妥協案として、「だいたいイイんじゃないの」の定義として次を採用します。
- いくつかのモデルに関して、与えられたホーア式がすべて成立する。
「いくつか」はもちろん有限個です。有限個のモデルで調べても、正しさの保証には全然なりません。が、人間とコンピュータが現実的・実務的にできることは、まーソンナモンでしょう。しょうがないのです。
ホーアテスト
「プログラムの正しさ」の記述として与えられたホーア式を、証明することは諦めます。すべてのモデルに関して検証することも諦めます。適当に（恣意的かもしれません）有限個のモデルを選んで、それに関して検証することでヨシとします。このような検証行為をホーアテストと呼ぶことにします。ホーアテストはプログラムの正しさを保証しません。しかし、プログラムを正しくしようという意志の表現になり、プログラムが正しいことの状況証拠は与えます。
もう少し正確にホーアテストを定義しましょう。ホーア式をいちいち三つ組で書くのは面倒なので、α、βなどのギリシャ小文字で表現します。α = p{f}q とかですね。Mがモデルだとして、ホーア式αがモデルMに対して妥当であることは M |= α と表します（標準的な記法です）。メタ命題 M |= α を現実に確認する行為を基本ホーアテストと呼びましょう。基本ホーアテストは、モデルMとホーア式αが指定されないとできません。また、その結果は真（テストが成功）か偽（テストが失敗）のどちらかに確定します*5。
基本ホーアテストの集合を（一般の）ホーアテストと呼ぶことにします。例えば、{M |= α, M |= β, N |= α} は、3つの基本ホーアテストを含むホーアテストです。次のルールで、ホーアテストの記述を簡略化することにします； 記号「|=」の左右に、カンマで区切ったモデル群、カンマで区切ったホーア式群を書くと、一度にたくさんの基本ホーアテストを記述したことになります（そう約束します）。例えば、M, N |= α, β, γ は次の6つの基本ホーアテストの集合を表します。
- M |= α
- M |= β
- M |= γ
- N |= α
- N |= β
- N |= γ
モデルと妥当性をどう定義するのか
基本ホーアテストは M |= α の形と言いましたが、モデル M と妥当性 |= の意味が確定しないと実際には使えません。モデルを考えるには、意味の世界と、記号の解釈が必要です。意味の世界としては、既に述べたように「非決定性写像の圏NDMpa＋ブール代数Ω(S)達」を考えます。しかしまだ、世界を指定しただけで、「その世界のナニをモデルMとするか」はハッキリしてません。
ホーアテストを現実的・実務的なものにするには、人やコンピュータが実際に遂行できるようにモデルと妥当性を選ばなくてはなりません。そこで次のようにします。p∈Ω(S), f:S→T, q∈Ω(T) から構成されるホーア式 p{f}q に適合するモデルとは：
- 圏NDMpaの対象（状態空間）Sと、Sの点（状態点）sの組のことである。
モデルは (S, s) という形で書けます。と、まー、これでもいいんですが、集合の要素sが出てくるのがなんか圏論ぽくないし、定式化もダサくなるので、次のように言い換えます。
- モデルとは、s:1→S という射のことある。1は特定された単元集合*6。
この定義では、モデルは s:1→S と書けます。
さて、モデル s:1→S に関してホーア式 p{f}q が妥当であるとは次のことだとします。
- s;(p・f) ⊆ s;(f・q)
等式的な定義の方が好きなら、次でも同値です。
- s;(p・f) = s;(p・f・q)
まとめておくと：
- [s:1→S |= q{f}q] ⇔ [(s;(p・f) ⊆ s;(f・q)] ⇔ [s;(p・f) = s;(p・f・q)]
踊り場の次は
これでだいたい「踊り場」の役割は果たしたと思います。次は、p, q などの条件とプログラムの実行 f の定義を少し変形した上で、エクスペクテーション・ベースのホーア式とホーアテストについて述べたいと思います。
