ソースコードの形式化 - (保存用) 檜山正幸のキマイラ飼育記メモ編

http://d.hatena.ne.jp/m-hiyama/20060119/1137641539の「モゴモゴな話」に書いた件でメモ：

少し分かってきた（かな？）。まず、関連するエントリーは：

↑ではKleisli構成を使っているが、もう一捻りして、Circ構成と組み合わせる。

Sign上のTermモナド

Σを多ソート指標とする。Op(Σ)はオペレータ記号の集合、だが、f∈Op(Σ)をf∈Σと略記。適当な規則で、Σ上の自由変数を含まない項の集合Term(Σ)を定義する。

t∈Term(Σ)にもt:s1,...,sn→tのようなソート付けができるとする。ΣのソートにTerm(Σ)を一緒に考えると再び指標となる（無限指標も許す）。この指標も同じくTerm(Σ)と表す。TermはSign上の自己関手となり、さらにモナドである。

Sign上のTermモナドがプログラミング言語の定式化である。Sign自体はIDLのようなものだ。

circ-Kleisli構成

Signは有限余完備とする。特に直和に関して対称モノイダル。

ΣとΓが指標のとき、α:Σ+Σ' → Term(Γ+Σ') in Signを新しい圏Progの射:Σ→Γと考える。Σ'はプライベート指標である。プライベート指標に関しての再帰ができる。α:Σ+Σ' → Term(Γ+Σ')とβ:Γ+Γ'→Term(Δ+Γ')の結合は、Σ+Σ'+Γ'、Γ+Σ'+Γ', Δ+Σ'+Γ' を考えて、適当に拡張した上でKleisli結合を作ればよい。

以上の構成は、対称モノイド圏上のモナドに関して実行できるだろう。特にIdentityモナドのときがCirc構成。通常のKleisli圏は、いま定義したcirc-Kleisli圏に埋め込める。

Prog圏

Signから作ったcirc-Klseili構成で作った圏をProg(Sign)と書く。Termモナドも明示するなら、Prog(Sign, Term)。Prog圏の射をプログラム形式と呼ぶことにする。

さて、問題はProg圏の意味論。Σにはモデル圏としてAlgΣ（無条件Σ代数の圏）が既に付いている。p:Σ→Γがあると、AlgΓの対象を実際に与えるとΣ代数を実際に構成できる（はず）。プログラム形式は、関手を定義する（関手意味論）。よって、SignとSign上のMod関手をProg(Sign)と拡張Mod関手に拡張できる。

しかし、Prog圏の構成から、代数のスパンとかがどっかで入る気もするが、、、要確認。

仕様との関係

あとはSenの拡張。SenΣ、SenΓ上のセオリーと、ΣをΓを使って定義するプログラム形式Σ→Γとの関係が欲しい。証明系がないとあまり意味がないからπインスティチューションが登場するだろう。何かの事例で考えないと。

とにかく

仕様、プログラムテスト、プログラム証明（ソースコードレビュー）、論理的証明（普通の証明）、ソースライブラリ／バイナリライブラリ、再利用（いろんな意味で）、正しさ(correctness)などの概念を定式化したい！それで結局、コンポネントって何だろう？コンポネントの圏を定義したーい！！