アメナブル性と境界付け

C = (C, ×, 1, σ, *, η, ε)がコンパクト閉圏だとして、f:A→Bに対して、fのネーム[f]:1→A×B* が決まる。しかし、[f]と[g]が同型でも、fとgは全然違うケースもある。この状況をJanusコンポネントの圏で考えてみる。

Janus profileからinputとoutputの別を取り除いてしまったものをundirected profileと呼ぶ。input/output（または右と左）の区別があるprofileを特にdirected profileとも呼ぶ。directed profile → undirected profile はまったく自明だが、与えられたundirected profileからdirected profileを作るのは簡単ではない。単に組み合わせ的にdirectionを選んでいいわけではない。

この事情にはアメナブル性やらシステム境界がからんでくる。profile（とそれを満たすコンポネント）がアメナブルであるとは、「観測子に副作用はない」ことである。これは指標の構文的な条件だけでは済まない。指標Σと部分指標Σ'があるとき、ホーア式を使ってAmenable(Σ, Σ')を書き下すことができる。観測子の部分指標Obs(Σ)が指定されているとき、(Σ, Obs(Σ))がアメナブルであることは、Amenable(Σ, Obs(Σ))として書ける。

単一のObs付きの指標Σをもとにしたアメナブルなundirected profileが与えられているとき、これを2つの部分指標Σ1とΣ2に分割して、どちらもアメナブルにするのが問題となる。イイカゲンに分割すればアメナブル性は壊れる。アメナブルな分割ができるかどうか？どのくらいの数の分割があるか？がプロファイルの単純さの基準となる。換言すると、アメナブルな部分プロファイルの大きさが尺度となる。

Janusコンポネント（のプロファイル）はアメナブルなものに限定していいだろう。アメナブル性がコンパクト閉圏の演算で保たれることを確認する必要があるが。

プロファイルの分割はシステム境界の設定でもある。単一境界のシステムを、複数境界のシステムとして配備できるか？ということだ。undirected profileをdirected profileにする作業は境界付けと呼んでよいだろう。

下手な境界付けはアメナブル性を壊す。これは、因果的に見えなくなることだと言ってもいいかもしれない。非アメナブル／非因果的なシステムは、制御不可能な見えない介入者がいるようにふるまう。