だんだん思い出した：指標＝インターフェイスの理論
あああああー、そうか。それをjanus〈ヤヌス〉と呼んでいたのだ。
プログラミング言語Lを、指標の圏Sigとその上のモナド L = (L, μ, η) と同一視する。つまり、プログラミング言語 ＝ (Sig, L) 。プログラミング言語 L = (Sig, L)のクライスリ圏 Kl(L) = Kl(Sig, L) をImplL と書く。以下、プログラミング言語全体をLで代表させる。
OpImplL を次のように定義する。
- OpImplL = (ImplL)op
Lを固定して、ImplLをImplと略記する。Implの射をソフトウェア実装、または単に実装と呼ぶ。指標Σごとに Mod[Σ] = [Σ*L, Set] が決まる。(-)*LはL-クリーネスターで、指標から圏を作る操作。Mod[Σ]は関手圏になる。Mod[-]:Impl→CAT はインデックス付き圏になる。
Ω∈|Impl|とMod[Ω]の対象mの対 (Ω, m) を（Lの）システムと呼ぶ。システムは、Mod[-]のグロタンディーク平坦化の対象である。システムを固定すると、Semm:Impl/Ω→Set というセマンティクスが決まる。このセマンティクスSemmは(Ω, m)による局所的なもので、全体的な構造を捉えてはいない。
目的は、プログラミング言語Lから、Janusコンポーネントの圏CmpntL を作ること。これは、ImplLに直和をモノイド積にしたトレース付きモノイド圏構造を入れて、そのInt構成〈GoI構成〉としてCmpntを作る。
圏Cmpntの対象は、有極指標〈polarized signature〉になる。有極指標を「顔」とみなして、コンポーネントには2つの顔（“表の顔”と“裏の顔"）があるので、ヤヌスにしたわけだ。
一連のストーリーで自明でない箇所は一箇所だけ。圏Implにトレースが入るかどうか？ あるモノイド圏Cがトレースを許容するとき、トレース許容的〈trace-admissible〉と呼ぶことにする。Cの拡張である圏〈super category〉Dがトレース許容的なとき弱トレース許容的〈weakly trace-admissible〉と呼ぶ。
Impl自体にトレースを入れるのは難しいので、Implの拡張Impl〜にトレースを入れて、Cmpnt = Int(Impl〜) と定義することになるだろう。
Impl〜上のトレースの構成とは、結局は再帰理論なので、コンポーネント構成のキモは、プログラミング言語Lがどの程度再帰を許すか、あるいは再帰の意味論がどこまで出来るか？にかかっている。
recursive languageは別な意味があるので、再帰が出来ることを recursion-capable とする。
- Lがrecursion-capable ⇔ ImplLがweakly trace-admissible
[追記]このフレームワークで、双模倣と森田同値、淡中再構成（再現）ができないか？ とか考えていたのだった、昔。淡中再現定理には、忘却関手（ファイバー関手）が必要だから、ファイバー関手を含めた構造を定義する必要がある。[/追記][さらに追記]次のエントリーも→論理におけるrecursion-capable - 檜山正幸のキマイラ飼育記 メモ編[/さらに追記]
