仕様証明とプログラム証明

インスティチューションがあって、Σ∈|Sign|ごとに、証明可能性“|-”が付いているとする。A⊆Sen(Σ)、b∈Sen(Σ)に対して、A|-b は、Aを仮定してbが証明できること。|-を拡張して、A|-Bが定義できる。「A|-B ならば A|⇒B」が健全性。ここで、A|⇒B は、BがAの帰結になっていること； ∀M.[M|=A ならば、M|=B]。これで、Mod(Σ)の部分圏の大きさを比較できる。

上のような仕様証明系が付いたインスティチューションがπインスティチューション。それに対して、Pインスティチューションに別な証明系がついたインスティチューションがπPインスティチューション。Σに対して、アサーションの集合Ass(Σ)を考える。Ass(Σ)の元は、適当な論理のformulaだと考える。ただし、Sen(Σ)⊆Ass(Σ)。これは、仕様の論理はそのままプログラムの論理に使えるってこと。

P⊆Sen(Π), S⊆Sen(Σ)として、Ass(Σ+Π)のなかで証明を考える。P|-Sであれば、プラットフォーム仕様がサービス仕様を満足する可能性を示すが、それでは面白くない。具体的な証明ネットΦ:P→Sが問題。証明ネットΦからプログラムを抽出する方法progがないとしょうがない。prog(Φ):Σ→Π となる（定義の都合で反変）。健全性は、「Φ:P→S ならば、prog(Φ)は(S, P)-correct」の形。

これらを定式化するには、πインスティチューションのセオリーの圏TheoをさらにPインスティチューションの文脈で拡張する必要がある。S=(Σ, S)（S⊆Sen(Σ)）、Pなどが仕様であるとき、プログラムを埋め込んだ証明ネットを射とする圏を作る必要がある。健全性から、Φ:P→S ならば、prog(Φ):Σ→Π in Progであるだけでなく、[[prog(Φ)]]:Mod(Π,P)→Mod(Σ,S) が定義可能。

健全なプログラム証明系があれば、[[prog]]: PProof →ModCat が定義可能。ここで、ModCatはCatの部分圏で、モデルとしてふさわしい圏を集めたもの。つまり、仕様|→モデル圏、プログラム証明|→モデル圏間の関手（プログラムを経由）と対応する。

もし、プログラミング＝プログラム証明行為なら、プログラムは仕様（制約、記述）の間の変換を与え、具体的・構成的にモデル関手（モデル圏のあいだの関手）を定義する。プログラムpのモデル関手PMod(p)がMod(Π)→Mod(Σ)で定義できるのは明らかだが、どんな部分圏に制限できるかが、深刻な問題なわけだな。

まとめ： インスティチューションの拡張としてPインスティチューションが作れるのと同様に、πインスティチューションからπPインスティチューションが作れる。πPインスティチューションには、プログラム証明の圏PProofが付いていて、その対象は、インスティチューションの仕様（Senの部分集合、公理系）またはセオリーである。prog: PProof→Progでプログラムの抽出ができる。progとプログラムの意味論[[p]]を組み合わせると、プログラム証明の健全性が定義できて、それは圏論的解釈ができる。

課題：圏PProofをちゃんと定義せよ。