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

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

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

参照用 記事

インスティチューションとホーア論理

「インスティチューションとホーア論理を一緒にしたようなナニカ」は、僕にとっての一つの課題です。この課題については、次のエントリーで述べています。

インデックス付き圏のフビニ/グロタンディーク同値」では、入れ子になったインデックス付き圏を持ち出しました。入れ子のインデックス付き圏の動機は「大量のモナド類似物(monad-like entities)を一挙に扱う方法」だと書きました。実は、「インスティチューションとホーア論理」を考える上でも、入れ子のインデックス付き圏が使えそうなのです。

内容:

  1. ホーアトリプルの圏
  2. インスティチューションの精密化
  3. 依存的なインデックス付き圏

ホーアトリプルの圏

以下の記述において、記号の使い方は、「インデックス付き圏のフビニ/グロタンディーク同値」と同様とします。

真偽構造が付いた圏とは、圏Cと反変関手 P:COrd の組 (C, P) のことです。ここで、Ordは順序集合の圏です。

順序集合はやせた圏とみなせるので OrdCat と思えば、(C, P) はインデックス付き圏です。(C, P) にグロタンディーク平坦化を適用できて、できた圏はホーアトリプルの圏になります。次のように書いてもいいでしょう。

  • Hoare(C, P) := Σ(x∈C | δx P[x])

Hoare(C, P) の対象は、C対象Aと命題p(p∈P[A])の組 (A, p) です。これは、「領域A上で解釈すべき命題p」と言えます。(A, p) から (B, q) への射は、p ≦ f*(q) という不等式で、これを集合ベースで解釈するなら次の論理式を表すと思っていいでしょう。(⊃ は含意記号。)

  • ∀x∈A.[p(x) ⊃ q(f(x))]

あるいは、意味論的に解釈して:

  • (x |= p) ⇒ (f(x) |= q)

A, Bを状態空間、fをプログラム実行による状態遷移と考えれば、たしかにホーアトリプルになっています。圏 Hoare(C, P) の射は、p{f}q : A→B のように書けます。

圏 Hoare(C, P) の射であるホーアトリプル p{f}q : A→B から、実行部分 f:A→B だけを抜き出す関手を射影として、Hoare(C, P)→C はファイバー付き圏になります。このファイバー構造まで含めたホーアトリプルの圏を考えれば、真偽値付き圏とホーアトリプルの圏は(圏同値の意味で)1:1に対応することになります。

以上のことから、真偽値付き圏は「ホーア論理が展開できる圏」とも言えます。そして、真偽値付き圏はインデックス付き圏の一種でした。

インスティチューションの精密化

インスティチューションは、インデックス付き圏に構造を追加したものとみなせます。そのことは次の記事を参照してください(系統的な説明じゃありませんが)。

Sigを指標の圏、Modを指標にモデル圏を対応させる関手とします。Mod:Sig→Cat なので、(Sig, Mod) はインデックス付き圏になります。通常のインスティチューションの定義では、Sigの対象Σに論理文の集合 Sen(Σ) を対応させる写像と、充足関係(satisfaction relation)を考えます。

ここでは、指標Σのモデル圏 Mod[Σ] を単なる圏ではなくて、真偽構造が付いた圏にします。真偽構造のベース圏を改めて Mod[Σ] と書き、Mod[Σ] 上で定義された真偽値(あるいは命題)の順序集合を対応させる関手を P[Σ] とします。(Mod[Σ], P[Σ]) が真偽構造付き圏で、これは指標Σごとに定まります。

σ:Σ→Γ が指標圏Sigの射だとすると、反変的にリダクト関手 σ*:(Mod[Γ], P[Γ])→(Mod[Σ], P[Σ]) が定まります。(Mod[Γ], P[Γ])→(Mod[Σ], P[Σ]) の関手とは、真偽値構造付き圏のあいだの準同型であり、通常の関手 F:Mod[Γ]→Mod[Σ] と、自然変換 ψ::F;(P[Σ])⇒P[Γ] からなります。

このような構造は、インスティチューションの精密化を与えていると期待できます。Senとその翻訳写像、充足関係などが出てきませんが、それらは上記の素材から再構成できると思われます。

[追記 date="2011-11-12"]いやっ、再構成できないかも。なんか足りてない。翻訳写像は、指標射と同じ向きなので、指標射と共変的に働くナニカが必要みたいです。[/追記]

依存的なインデックス付き圏

今述べたインスティチューションの精密化(と期待される構造)では、ベース圏としてSigがあり、真偽構造付き圏を値とするインデキシングの構造があります。しかし、「インデックス付き圏のフビニ/グロタンディーク同値」のように、それを二重インデックス付き圏に直すことはできません。

なぜなら、Mod[Σ] がΣごとに変わってしまうからです。Σによらず同じファイバーが生えているなら、ベース圏と典型ファイバーの直積上のインデキシングを構成できますが、そうはなっていません。Σに依存してファイバーが変わるのです。言うなれば、依存的なインデックス付き圏ですね。

しかしそれでも、「グロタンディーク平坦化の適用の順序によらず出来上がる圏は同値」という主張は意味を持ちます。「これが成立しているといいなー」と思ってますが、確認は出来てません。

いずれにしても、繰り返しされたインデキシングを持つような圏は、計算モデルにはよく出てくるみたいです。