「ホーア論理の圏論的な定式化」において、インスティチューションとホーア論理を一緒にしたようなナニカができないかなぁ、とか言ったので、もう少し考えてみることにします。ただし、最初のステップだけで、インスティチューションを使う段階には至ってません。
僕がやりたいことは、「拡張されたホーア論理」の意味論を構成することですが、とりあえず意味論の舞台となる構造を作ることにします。真偽値という概念を圏論的に扱いやすい形にしたモノです。
内容：
圏の上に真偽値を乗せる
アブラムスキー達の仕様構造（specification structure）では、圏Cの対象AごとにP(A)という集合が対応してます。P(A)とは何かというと、（非形式的な想定としては）領域A上の性質（properties）、述語（predicates）でしょう。一番分かりやすい例は、P(A) = Pow(A)（ベキ集合）です。いずれにしても、property, predicate, powerですから頭文字は'P'。
以下では、P(A)を真偽値の集合だと考えます。真偽値とは言っても二値とは限らず、正しさの度合いを測る何らかの量のことです。真偽値の集合はブール代数やハイティング代数*1の構造を持ちますが、ここではとりあえず順序集合と考えます。つまり、P(A)は順序集合の圏Ordの対象となります。さらに、Pは反変関手となっているとします。P:Cop→Ordです。Cが集合圏の部分圏でPが反変ベキ集合関手のときが典型的な例です。
圏Cと反変関手 P:Cop→Ordの組み合わせ (C, P) をC上の真偽構造と呼ぶことにします。真偽構造は仕様構造と同じではありませんが、真偽構造から仕様構造を作り出すことができます。
Cの仕様構造は、A∈|C| ごとに割り当てられたP(A)と、ホーアトリプルの集合族 H(A, B) （A, B∈|C|）によって決まります（「ホーア論理の圏論的な定式化」参照）。(p, f, q)∈(P(A)×C(A, B)×P(B)) がホーアトリプルである条件を次のように定めます。
- p ≦ P(f)(q) in P(A)
Pは反変関手であるので、P(f):P(B)→P(A) in Ord となり、P(f)(q) はP(A)の要素として定まります。P(A)は順序集合なので不等式も意味を持ちます。よって、この定義はwell-definedです。定義をまとめておくと：
- p{f}q ⇔ (p, f, q)∈H(A, B) ⇔ p ≦ P(f)(q)
以下のホーアトリプルの公理が満たされることは簡単に確認できます。
- p{id}p
- p{f}q, q{g}r ならば p{f;g}r
これらのことから、真偽構造は仕様構造の特殊なモノとみなせることがわかります。より正確に言えば、真偽構造に対して標準的に（canonically）仕様構造を対応させることができ、この対応を経由して仕様構造に関するすべての結果が真偽構造にも適用できます。
真偽構造のあいだの準同型
(C, P) と (D, Q) が2つの真偽構造のとき、このあいだの準同型を定義します。以下の定義はお決まりの手順といえます。
まず、F:C→D という関手をベースにします。真偽構造のQも関手 D→Ord でした。FとQをこの順で結合すると、F;Q:C→Ord という反変関手となります（面倒なので、いちいち -opを付けるのはサボリます）。つまり、F;Q はC上の真偽構造となります。
PもF;Qも、関手圏 [Cop, Ord] の対象です。この2つの関手を繋ぐ自然変換 ψ:P→F;Q を考えることができます。共変関手 F:C→D と、自然変換 ψ:P→F;Q の組 (F, ψ) を (C, P) から (D, Q) への準同型とします。これが真偽構造のあいだの射です。
大きさ（smallness）に関するデリケートな議論は無視することにすれば； すべての真偽構造とそのあいだの準同型は圏となります。Ord値関手付きの圏を対象として、引き戻し関手と関手間の自然変換を射とする圏ですね。
具体的な真偽構造付き圏
一般的な真偽構造付き圏では漠然としているので、ホーア論理、すなわち「プログラムの実行文と表明」に関する意味論で使うの事を想定して、より具体的な圏の事例を挙げます。
圏Cの対象は集合とします。プログラムの意味論では大きな集合は不要なので、高々可算な集合としておいてもいいでしょう。射は部分写像とします。全域写像を要求すると計算の議論はうまくいきません。お好みに応じて、射を非決定性写像としてもいいです。
真偽構造を与える関手Pは、反変のベキ集合関手とします。ベキ集合は包含順序を持つので、自然に圏Ordの対象とみなせ、P(f) は順序を保つので、P:C→Ord とみなせます。実際には、集合論的ベキ集合は超越的過ぎるので、「計算可能な部分集合」に限るのが自然だと思いますが、まー、それは気にしない方向で。
圏Cの対象である集合は、気持ちとしては状態空間とみなします。Cの射は状態遷移です。状態遷移は、必ずしも同じ状態空間のなかで起きるのではなくて、異なる状態空間に遷移することもあります。例えば、実行時にメモリーアロケーションをすれば、プログラムの状態空間自体が変わってしまうことがあるので、f:A→B （A ≠ B）のような状態遷移は別に特殊なモノではありません。
真偽構造Pによる P(f):P(B)→P(A) は、状態遷移fに伴う真偽値の変換を表します。真偽値とは言っても、二値とは限らず、拡がりをもった真偽値＝部分集合となっています。状態遷移はプログラミングレベルの概念ですが、関手Pにより真偽値変換という論理レベルの解釈も可能となっているのです。
拡張されたホーア論理
冒頭で「拡張されたホーア論理」という言葉を出したのですが、どう拡張する（心積もり）かというと、型付きホーア論理、あるいは多ソートホーア論理とでもいう形で、型システムを考慮することにします。
型（ソート）は圏の対象にマップされます。そして、表明の条件は真偽値に、実行文は射にマップされるのです。逆に言うと、型付き（多ソート）ホーア論理の意味論にふさわしい意味領域として、真偽構造付き圏が必要になるのです。
拡張されたホーア論理とその意味論はまたいずれ。
*1:http://ja.forvo.com/search/Heyting/ によると、オランダ語のHeytingはヘイティンと聞こえます。
