Pインスティチューション

インスティチューションにプログラム（のソースコード）とプログラム証明を入れる準備。

Pインスティチューションとは、(Sign, Mod, Sen, Prog, PMod, |=)であり、ProgとPModを除くとインスティチューション、Sign⊆Progであり、iが包含として、i;PMod = Mod。つまり、Prog, PModがSign, Modの拡張になっている。しかし、Senの定義をProgまで拡張できることは仮定されてない。Senが部分圏でしか定義されてないインスティチューションともみなせる。

f:Γ→Σ in Progは、プラットフォーム指標Σを使って(use Σ)、サービス指標Γを提供する(provide Γ）実装コードである。P⊆Sen(Σ)、S⊆Sen(Γ)だとして、A∈Mod(Σ) が A|=P ⇒ [[f]](M)|=S であるとき、fは(S, P)-correctということにする。fが(S, P)-correctなら、fの意味[[f]]は、Mod(Σ; P)→Mod(Γ; S)関手だと解釈できる。(S, P)-correctはメイヤーの契約概念で、プラットフォーム（動作、仕事の環境）がPを満たす条件でプログラムはサービスSを顧客に提供する義務を負う。

Pインスティチューションからプログラム証明系を作ることが課題。プログラムfから証明木（または証明ネット）Φが作れて、ΦがPからSへの証明ならfが(P, S)-correctである。(P, S)-correctを(P, S)|= fとすると、P |- S by f ⇒ (P, S)|= f。逆に、(P, S)|= f ⇒ P|-S by f なら完全なプログラム証明系。ここはゲンツェン・スタイルがいいような気がする。

なんで、「P」か？ なんとなく。 πインスティチューションがあるけど、ギリシャ文字よりローマ字がいい、ProgのP、partialのPかも。