仕様とプログラム証明の圏 - (保存用) 檜山正幸のキマイラ飼育記メモ編

少し前にセオリーと証明の圏 - 檜山正幸のキマイラ飼育記メモ編というのを書いたし、随分以前にPProofを問題にしていた。

最近、仕様とプログラム証明の圏がやっとわかった気がする。この圏の対象は仕様(Σ, A)（A⊆Sen(Σ)）。射の定義が問題なのだ。射を定義するために、適当なプログラミング言語PLを固定して、そのプログラミング言語に関するプログラム証明の体系を作る。この体系を（PLに関する）プログラム論理と呼ぶ。PLogをプログラム論理として、これを指標Σで拡張したものをPLog(Σ)とする。PLog(Σ)の文をPSen(Σ)とする。PSen(Σ)にはプログラミング言語PLの文（実行文）も埋め込まれている。

さて、(Σ, A)から(Γ, B)への射は、文（論理式）の集合の余スパンである。余スパンを構成する写像を左脚／右脚と呼ぶことにする。余スパンのボディはPSen(Σ)とする。Sen(Σ)→Psen(Σ)という埋め込みがある。これが左脚になる。文集合AのPSen(Σ)への埋め込み像も同じ記号Aで示す。

問題は右脚。プログラム形式（ソースコード）は、Γ→PTerm(Σ)というKleisli射を定義するが、これを使うと、指標Γの文を、指標Σとプログラミング言語PLが混ざったモノに変換できる。つまり、プログラム形式は、Sen(Γ)→PSen(Σ)を定義する。これを右脚に使う。

プログラム形式pが定義するSen(Γ)→PSen(Σ)をp*として、Bのp*による像をp*(B)と書く。PLog(Σ)は論理系だから、A⊆PSen(Σ), p*(B)⊆PSen(Σ)が与えられれば、その証明（が可能ならば、それ）が存在する。証明をαとする。αは、A|-p*(B) in PLog(Σ) を保証する。

で、いよいよ射の定義：(Σ, A)→(Γ, B)は、Γ→Σ（意味的には逆向きか）のプログラム形式pとPLog(Σ)のなかの証明αで定義される。その条件は：

αにより、A |- p*(B) である。

項モナドPTermや論理系PLogを定義するときに、パラメータとしてプログラミング言語を渡す。よって、仕様とプログラム証明の圏PProofは、プログラミング言語によってindexingされるだろう。

もう少し厳密に定義するには、論理系（証明系）の余スパンの構成が必要になる。とりあえず、証明系はムーア閉包作用素を持った文集合で定義すればいいだろう。以前から余スパンが関係するとは思っていたから、これはいい方向への進展だろう。