コンストラクタやクローニングの表示的意味論：多オブジェクト系とフォック構成 (1)

「メイヤー指標」において：

Creatorはオートマトン（ラベル付き状態遷移系）の状態遷移と考えることはできません。複数のオートマトンの状態を同時に表現できるような空間、いわばオートマトンのフォック空間（Fock space）を考えて、フォック空間内でオブジェクト（粒子）を増やすオペレーションとして定義するべきだろう、と思ってます。あまりハッキリと見えてはないのですけど。

しばらく考えたら、だいたいの事情はわかりました。本来の「Command-Query分離の原則」ではCreatorは扱わないのですが、Creatorを含む指標の表示的意味論（の一例）を組み立ててみます。書いているうちに長くなってしまったので、今回は予備知識と方針の確認です。

内容：

指標モジュール
オブジェクト指向とメイヤー指標
メイヤー指標の余代数意味論
Creatorの意味論

言葉使いに関する注意

指標は、「ソート記号の集合」と「オペレーション記号の集合」から構成される構文的な対象物です。構文的（意味的ではない）ことを強調する意味で「記号」を付けていたのですが、面倒なので、ソート記号を単にソート、オペレーション記号を単にオペレーションと呼ぶこともあります。

ソートとオペレーションはあくまで記号なので、対応する意味領域の存在物は、型と関数と呼ぶことにします。一般的には、型は圏の対象で、関数は圏の射です。意味領域として採用できる圏には、Set（集合圏）、Partial（部分写像の圏）、Rel（関係の圏）、Ord（順序構造の圏）、Top（位相空間の圏）などの圏の部分圏があります。意味領域となる圏を特定はしませんが、例えば、Partialのなかで、対象を“たかだか可算集合”に限定した部分圏とかが適切です。

ソートの集合が可視ソートと隠蔽ソートに分割された多ソート指標を隠蔽多ソート指標と呼ぶことにします。メイヤー指標は、隠蔽多ソート指標の特別なものです。

指標の記述方法

次は、「メイヤー指標」で出した指標の例、スタックの指標です。

hidden sorts : Stack;
visible sorts : Value, Boolean, Error, OK;

signature global() {
  creator newStack :: -> Stack;
}

signature stack(Stack) {
  command push :: Value -> Stack;
  command pop :: -> [Stack, (OK | Error)];
  query top :: -> (Value | Error);
  query isEmpty :: -> Boolean;

  creator clone :: -> Stack;
}

今回もこの書き方を使うことにします。書き方の注意点をまとめておくと：

ソートの宣言は指標（signature）ブロックの外側に書く。
宣言された基本ソート以外に、基本ソートを組み合わせた複合ソートも認める。複合方法は直積（タプル、リスト）と直和（排他的ユニオン）である。
メイヤー指標には、主要ソートと呼ぶ隠蔽ソートが1つだけ定まっている。主要ソートは指標名の後の括弧内に書く。
主要ソートがない指標（上の例ではglobal）も認める。
主要ソートを持つ指標のオペレーションでは、その第1引数ソートは常に主要ソートとなるが、オペレーション宣言では第1引数を省略する*1。

若干の変更：

-> Stack のように矢印の左側を省略すると分かりにくいかもしれないので void を導入する。-> Stack と void -> Stack は同じ。
Creatorオペレーションの戻り値ソートが隠蔽ソートなら、ソートの直後に「as 指標名」と書ける。これは、戻り値に指標名で宣言されているオペレーションを適用してよいことを示唆する。

この変更を導入して上の例を書き換えると次のようになります。

hidden sorts : Stack;
visible sorts : Value, Boolean, Error, OK;

signature global() {
  creator newStack :: void -> Stack as stack;
}

signature stack(Stack) {
  command push :: Value -> Stack;
  command pop :: void -> [Stack, (OK | Error)];
  query top :: void -> (Value | Error);
  query isEmpty :: void -> Boolean;

  creator clone :: void -> Stack as stack;
}

ここでは、command push :: Value -> Stack; のように、戻り値ソートでは隠蔽ソートを明示的に書いています。しかし、主要ソートである隠蔽ソートは戻り値側でも省略することもあります。その流儀だと、command push :: Value -> void; となります。主要ソートをどこまで省略するか／しないかは趣味の問題ですね。

指標モジュール

メイヤー指標の場合、唯一の主要ソートを持つことが条件になっているので、複数の指標をひとつの指標にまとまることが出来ません（一般的な隠蔽多ソート指標なら可能です）。そこで、複数の指標をそのまま複数のモノとして扱います。いくつかの指標の集まりを指標モジュールと呼ぶことにします。

以下の例は、整数値を積むスタックの指標とカウンターの指標を含む指標モジュールです。（意味が定義されてないので、スタックやカウンターの実際の挙動は未定ですが。）

hidden sorts : Stack, Counter;
visible sorts : Integer, Boolean, Error, OK;

signature global() {
  creator newStack :: void -> Stack as stack;
  creator newCounter :: void -> Counter as counter;
}

signature stack(Stack) {
  command push :: Integer -> Stack;
  command pop :: void -> [Stack, (OK | Error)];
  query top :: void -> (Integer | Error);
  query isEmpty :: void -> Boolean;

  creator clone :: void -> Stack as stack;
}

signature counter(Counter) {
  command inc :: void -> Counter;
  command dec :: void -> Counter;
  command reset :: void -> Counter;
  query value :: void -> Integer;
}

オブジェクト指向とメイヤー指標

メイヤー先生はオブジェクト指向の人なので、「Command-Query分離の原則」もオブジェクト指向の文脈で語られています。通常のオブジェクト指向とメイヤー指標はどういう関係になるのでしょうか。

クラスは、状態空間Sとその上の関数（集合のあいだの写像）を定義すると考えましょう。Command（の意味）は状態遷移 S→S という関数です。Commandが引数を持つなら、その引数の型（に対応する集合）をAとして、S×A→S です。Query（の意味）は S→V という関数です。ここでVは、Queryによる観測値の集合です。Queryが引数を持つなら、S×A→V という形になります。

メイヤー指標の主要ソートは、クラスの状態空間に割り当てられる記号です。特殊な変数this（あるいはself）が走る領域が状態空間Sで、ソートはその状態空間の名前と考えることができます。指標に含まれるオペレーション（CommandまたはQuery)が、状態空間上の遷移と観測に名前を与えることになります。

実際のオブジェクト指向プログラミング言語の多くでは、指標とその主要ソートを一体のものとして扱います。別な言い方をすると、指標の名前と主要ソートの名前を同じにして同一視しているのです。さらに、指標に対する特定の実装も同じ名前で呼ぶことがあります。むしろ、実装（モデル）が先にあって、指標はそれに付随するオマケのようなもので、あまり意識されないこともあります。

ここでは、ソートと指標は別物として扱います。また、指標とそのモデル（実装）も区別します。煩雑になるようですが、こうした区別をすることにより事情がクリアになります。メイヤー指標の場合は、指標に対して主要ソートが一意的なので、指標とソートを一体のものとして扱えます。さらに、メイヤー指標に特定のオートマトン（状態空間＋遷移＋観測）を割り当てれば、指標とそのモデルが一体化した構造になります。

メイヤー指標の余代数意味論

指標に対して意味を与える意味領域として圏Cを固定します。圏Cは具象圏（対象は集合）だとして、直積、直和、指数（ベキ）を持つとします。Creatorを含まない（CommandとQueryだけから構成される）メイヤー指標Σを取ると、Σのモデル（意味）は圏C上の余代数として与えることができます。

余代数とは次のようなものです； F:C→C を圏C上の自己関手とします。F-余代数は、Cの対象Sと、射 f:S→F(S) in C の組 (a, f) です。定義はこれだけです。余代数を定義するには、事前に自己関手Fを決める必要があることに注意してください。

メイヤー指標Σから余代数を作る手順を簡単に説明します。まず、Σで使っている可視ソートにはCの対象を事前に割り当てておきます。これにより、可視ソートは型定数（集合定数）として扱えます。メイヤー指標Σの主要ソートをsとして、記号sの意味はCの対象（集合）Sだとします。

Command、Query達にも意味を与えて、c₁:S×A₁→S, c₂:S×A₂→S, ..., c_n:S×A_n→S, q₁:S×B₁→V₁, q₂:S×B₂→V₂, ..., q_m:S×B_m→V_m in C だとします。

ここでちょっとしたトリックを使います。Commandの意味である射 c_i:S×A_i→S を c'_i:S→[A_i, S] に変形します。[A_i, S] は指数です。Cに指数があると仮定したのでこの変形（カリー化）ができます。同様に、Queryの意味である q_j:S×B_j→V_j も q'_j:S→[B_j, V_j] と変形できます。

この変形の結果、c'_i:S→[A_i, S] （i=1, 2, ..., n）、q'_j:S→[B_j, V_j] （j=1, 2, ..., m）という (n + m)個の射ができます。これらの射はすべて S→ナニカという形をしてます。ここで自己関手 F:C→C を次のように定義します。

F(X) := [A₁, X]×[A₂, X]× ... × [A_n, X]×[B₁, V₁]×[B₂, V₂]× ... ×[B_m, V_m]

この定義は、対象Xに対しての定義ですが、定数ベキと掛け算（直積）しか使ってないので共変関手に拡張できます。この自己共変関手Fは、指標Σから自動的に定義できるので、F = F_Σ としましょう。CommandとQueryの意味であるCの射の集まりから、f:S→F_Σ(S) という余代数が構成できます。逆に、自己関手F_Σの余代数があれば、それをCommandとQueryの集まりにバラすことができます（直積の射影を取ります）。

自己関手F:C→C に対するF-余代数の全体は再び圏を構成します。この圏を Coalg(F:C→C)、あるいはより簡単に Coalg(F) と書くことにします。メイヤー指標Σに対する余代数圏 Coalg(F_Σ) を作れますが、この圏はだいたい「インターフェイスΣの実装からなる圏」と言えます。この圏の射は、オートマトン（ラベル付き遷移系）の模倣や双模倣に対応します。

Mod[Σ] := Coalg(F_Σ) として、Σを動かしてやると、メイヤー指標でインデックス付けされた圏の族ができます。メイヤー指標の全体に適切な圏構造を入れれば、Mod[Σ]はインデックス付き圏となります。さらに論理式による仕様記述を付け加えるとインスティチューションが出来上がるのです。

以上が、メイヤー指標の余代数意味論の大ざっぱなシナリオです。

Creatorの意味論

CommandとQueryだけから構成されるメイヤー指標に関しては、上記のような余代数意味論が構成できます。継承とかリスコフの置換原則なども、この枠内で説明できます。（僕が勘違いしてなければ）マイヒル／ネロードの定理も成立します。

ところが、Creatorが入ると、上記のような余代数意味論からハミ出してしまうのです。先に挙げた例では3つのCreatorが登場します。

signature global() {
  creator newStack :: void -> Stack as stack;
  creator newCounter :: void -> Counter as counter;
}

signature stack(Stack) {
  creator clone :: void -> Stack as stack;
}

voidに対応する集合は単元集合1とします。隠蔽ソートStackとCounterに、S、Cという実際の集合を割り当てたとして、Creatorオペレーションの意味は、[(newStack)]:1→S, [(newCounter)]:1→C, [(clone)]:S×1→S in C となります。ここで、[(…)] はスコット・ブラケットのつもりで、「…の意味」と読みます。さて、cloneの意味が変だと思いませんか？ S×1 はSと同一視していいので、S→S となりますが、これじゃ状態遷移を引き起こすCommandと区別が付きません。

cloneは1つのオブジェクトを2つにするので、S→S×S のはずです。S×S はオブジェクトが2個ある状態です。S×S×S なら3個のオブジェクト。つまり、何個かのオブジェクトがあって、個数が増えたり減ったりする状況を扱う必要があるのです。物理で（って、物理苦手だけど）多体系（多粒子系）って概念がありますが、同様に多オブジェクト系を考える必要があるようです。

多オブジェクト系の状態空間を構成できれば、Creator（コンストラクタやクローニング）もこの状態空間上の状態遷移として表すことができるでしょう。そうすれば、多オブジェクト系も通常の余代数意味論のなかに再び取り込める可能性も見えてくるでしょう。

（僕の気力が失せなければ）次回は、多オブジェクト系の状態空間を構成します。

*1:Catyでは、主要ソートを第0引数として扱ってます。また、可視ソートを主要ソートにすることを許しています。