正しさ

πPインスティチューションからあらためて見て、“既に動いている実装の正しさ”と“プログラムソースコードの正しさ”は別な概念だな。

実装が正しいとは仕様に対する充足性の問題で、たぶんvalidというのだろう。一方プログラムの正しさは、メイヤーの契約のようなもので、基礎となるプラットフォームがvalidである前提で要求を満たすことであり、こちらはcorrectかな。

言葉の問題はどうでもいいとして、仕様Sに対して正しい実装の全体はMod(Σ; S)⊆Mod(Σ)となり、Pを前提にSを提供する正しいプログラムpは、Mod(Π; P)→Mod(Σ; S) で解釈される。よって、Prog(Σ, Π)はFuctor(Mod(Π), Mod(Σ))と対応する。Prog(Σ, Π)にもFunctor(Mod(Π), Mod(Σ))にも、順序のような構造が入って、実はenrichedなのではないだろうか？

とりあえず、Prog(Σ, Π)には、最適化のようなプログラム変換があるのだから、2圏と考えるのは自然だし。