このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ホーア論理の圏論的な定式化

ソフトウェアの形式手法では、なにかしら論理の力の借ります。論理には、ウンザリするほどの種類がありますが、コンピューティングに利用するなら、ホーア論理が一番基本的で一番役に立つものだと思います。

ホーア論理の圏論的な定式化というと、アブラムスキー達による仕様構造(specification structure)という概念があります。例えば、次の論文の冒頭に仕様構造の記述があります。

仕様構造をベースにして、少し拡張した形で圏C上のホーア論理を定義してみます。

内容:

  1. 仕様構造
  2. プロパティのあいだの順序
  3. 引き戻し
  4. インデックス付き圏
  5. インスティチューション

仕様構造

C上の仕様構造の定義は簡単です。

  1. C対象Aごとに P(A) という集合が対応している。
  2. C対象A, Bごとに P(A)×C(A, B)×P(B) の部分集合 H(A, B) が対応している。

P(A)は、A上のプロパティ(properties over A)の集合と呼びます。H(A, B) はホーアトリプルの集合と呼びましょう。P(-) と H(-, -) に関して次の条件を要求します。

  1. (p, idA, p)∈H(A, A)
  2. (p, f, q)∈H(A, B) かつ (q, g, r)∈H(B, C) ならば、(p, f;g, r)∈H(A, C)

Cの対象はなんらかの領域であり、P(A)は領域A上で定義された述語(真偽値を値とする関数)の集合だと解釈するとわかりやすいでしょう。H(A, B) に含まれる3つ組 (p, f, q) は p{f}q と書きます。p{f}q と書いたら、(p, f, q)∈H(A, B) を暗黙に仮定します*1

p{f}q の意味は「x∈A が p を満たすなら、f(x) は q を満たす」と解釈すると、確かにホーアトリプルだと思えます。もちろん、この解釈は説明のための一例であり、仕様構造の定義は公理的に与えられます。

C上に仕様構造(ホーア構造と言ってもいいでしょう)(P, H) があると、新しい圏Dを次のように作れます。

  1. Dの対象は、A∈|C|、p∈P(A) の組 (A, p) である。
  2. Dの射 φ:(A, p)→(B, q) は、ホーアトリプル p{f}q である。

Dが実際に圏となることは、仕様構造の条件から保証されます(確認してみてください)。

プロパティのあいだの順序

仕様構造の条件は、ホーア論理における次のような公理(仮定無しの推論)と推論規則に対応しています。

-----------[skip]
p{skip}p


p{Γ}q q{Δ}r
-----------------[seq]
p{Γ;Δ}r

skipは「なにもしない」プログラムに対する表明で、seqはプログラムの順次結合に関するホーアトリプルの合成規則です。

p⊃q が含意を表す論理式だとして、通常のホーア論理では次の推論も許されます。


p⊃q q{Δ}r
----------------[limpl]
p{Δ}r


p{Γ}q q⊃r
----------------[rimpl]
p{Γ}r

C上の仕様構造に、このような含意を使った推論も取り入れましょう。そのためには、Aのプロパティの集合P(A)を順序集合にします。順序を「≦」で表すことにします。そして、仕様構造の条件に次を加えます。

  1. p≦q、(q, g, r)∈H(A, B) ならば、(p, g, r)∈H(A, B)
  2. q≦r、(p, f, q)∈H(A, B) ならば、(p, f, r)∈H(A, B)

引き戻し

A, Bが領域で、P(A), P(B) がその上の述語の集合のとき、写像 f:A→B があると、f*(q) = f;q として、f*:P(B)→P(A) を定義できます。f と f* の両方を使いたいことがあるので、これも入れて仕様構造をさらに拡張します。以下でOrdは順序集合の圏です。

  • f:A→B in C に対して、f*:P(B)→P(A) in Ord が対応していて、この対応が COrd の反変関手になっている。

通常のホーア論理において、ホーアトリプル p{f}q の成立は次のように言い換えられます。

  • x∈A が p を満たすなら、f(x) = y となる y∈B は q を満たす。

これを集合の逆像と包含関係で表現するなら:

  • {x∈A| p} ⊆ f-1({y∈B|q})

少し抽象化した状況に持っていくと、次のように書けます。

  • p≦f*(q)

プロパティの順序と反変関手の言葉で書けば次になりますね。

  • p{f}q ⇔ p≦f*(q)

インデックス付き圏

P:|C|→|Ord| と (-)*:CopOrd の組は、CからOrdへの反変関手を定義します。記法を簡略化するために、記号Pで反変関手を表すことにします。つまり、P:CopOrd

ここで、順序集合Xは圏とみなせることを思い出してください。圏とみなしたXの対象は集合Xの要素で、x≦y のとき x→y という射があるとします。とすると、P:CopOrd という反変関手の余域を、OrdからCatに切り替えることができます。同じ記号Pで余域を切り替えた反変関手を表すと、P:CopCat

余域がCatである反変関手はインデックス付き圏(indexed category)です。インデックス付き圏の話は「インデックス付き圏のグロタンディーク構成」とかに書いてあります。

すぐ上に出てきた「p≦f*(q)」という条件を反変関手Pを使って表現するなら、p≦P(q) ですが、順序≦は圏の射となるので、同値性「p{f}q ⇔ p≦f*(q)」は次にように書き換えられます。

  • p{f}q ⇔ (p→P(q) という射が存在する)

ホーアトリプル p{f}q とは、圏C上の仕様構造から作った圏Dの射でした。一方で、「p→P(q) という射」とはインデックス付き圏からグロタンディーク構成した圏の射です。結局、次の事実に行き着きます。

  • ホーアトリプルとは、仕様構造からグロタンディーク構成した圏の射である。

インスティチューション

話は変わってインスティチューション; インスティチューションは、ベースの圏をインデックスとするインデックス付き圏です。ベースの圏の対象を指標(signature)と呼びますが、指標は、いくつかのプログラミング言語では「インターフェース、型クラス、コンセプト」などと呼ばれているモノに対応します。その上に生えている圏はモデル圏(実装の圏)です。一方の仕様構造では、生えている圏はプロパティの圏です。プロパティの圏は「命題と証明の圏」と言い換えてもいいでしょう。

インスティチューションも仕様構造(ホーア構造)もインデックス付き圏で、生えている圏(ファイバー)はかたや意味論的、かたや構文論的です。この2つを関連付けられそうなんですが、なんかズレがあるんですよね。インスティチューションと仕様構造では、住んでいる世界のレベルが違うというか…。もう少し考えてみます。

*1:こういう「暗黙の仮定」は誤解や混乱のもとになったりするので、あまりよろしくないのですけどね。