メイヤー指標

メイヤー先生や、先生の「Command-Query分離の原則」については、何度も何度も話題にしてます。

「メイヤー」を含む記事一覧

最近（2012年）は、「Command-Query分離の原則」の代数的／圏論的な定式化をして、それに勝手に「メイヤー代数」だの「メイヤーオートマトン」だのと名付けています。ここでは、メイヤーオートマトンの仕様を与えるメイヤー指標について述べます。

内容：

多ソート指標
実用的な機能：ソートの項と名前付き指標
隠蔽ソートと可視ソート
メイヤー指標
メイヤー指標の意味付けはどうする

多ソート指標

指標（signature）とは、インターフェースをいくぶん抽象化したようなものです。指標は、ソート記号とオペレーションの宣言からなります。とりあえずは記号的な構成物で意味は後から与えます。

まず、Sはソート記号の集合とします。「ソート記号」とは何か？というと、それは定義しません。インフォーマルには「値の集合」を表す記号や名前だと思ってください。そして、Oはオペレーション記号の集合です。オペレーション記号が何であるかも未定義です。インフォーマルには、関数やメソッドを表す記号や名前です。f∈O に対して prof(f)∈(S^*×S) が定義されています。つまり、profは O→S^*×S という写像です。ここで、S^* はSのクリーネスターです。S^* は成分が集合Sに属するリストの集合だと思っても同じです。

オペレーション記号fに対してprof(f)は、fのプロファイルと呼びます。プロファイルの代わりにランクとかアリティと呼ぶこともあります。prof(f)は、S^*の要素と、Sの要素のペアです。((s₁, ..., s_n), t) の形をしてますが、これを、s₁, ...., s_n -> t と書くことにします。prof(f) = (s₁, ...., s_n -> t) であることを、

f :: s₁, ...., s_n -> t

と書きましょう。そして、f :: s₁, ...., s_n -> t という記述をオペレーション宣言と呼びます。

(S, O, prof:O→S^*×S) という3つ組が指標です。もう一度繰り返すと：

Sはソート記号の集合です。
Oはオペレーション記号の集合です。
f∈O に対して、prof(f)はfのプロファイルです。

SもOも有限集合だとして、S = {s₁, ..., s_k}、O = {f₁, ..., f_n} とします。σ_i∈S^* として、指標を次の形で書くことにします。ここではコロン2つ（'::'）を使っているので注意してください。



{

  sorts : s₁, ..., s_k;
  operation f₁ :: σ₁ -> t₁;

  ...

  ...

  operation f_n :: σ_n -> t_n;

}

実例をひとつ挙げておきます（毎度お決まりのスタックです）。



{

  sorts : Stack, Value, Boolean;
  operation push :: Stack, Value -> Stack;

  operation pop :: Stack -> Stack;

  operation top :: Stack -> Value;

  operation isEmpty :: Stack -> Boolean;

}

実用的な機能：ソートの項と名前付き指標

スタックの例を見てわかると思いますが、前節の指標の定義だと表現力に不足を感じます。

基本的なソート記号を組み合わせて、より複雑なソートを作りたい。

そこで、sorts で宣言された基本記号からソートの項（term, expression）を作ってもいいことにします。項形成規則（term forming rules）は色々と考えられますが、タプル（直積） [S, T] と排他的ユニオン（直和） (S | T) くらいは入れておくことにします（詳細はいま定義しない）。

ソートの項を使ってスタックの指標を書きなおすと：



{

  sorts : Stack, Value, Boolean, Error, OK;
  operation push :: Stack, Value -> Stack;

  operation pop :: Stack -> [Stack, (OK | Error)];

  operation top :: Stack -> (Value | Error);

  operation isEmpty :: Stack -> Boolean;

}

エラーの扱いがやや技巧的ですが、例外の宣言をきちんと導入すれば、もっと適切に表現できます。

複数の指標を扱うときは、それぞれに名前が付いていると便利です。次の形式で指標に名前を付けることにします。



signature stack {

  sorts : Stack, Value, Boolean, Error, OK;
  operation push :: Stack, Value -> Stack;

  operation pop :: Stack -> [Stack, (OK | Error)];

  operation top :: Stack -> (Value | Error);

  operation isEmpty :: Stack -> Boolean;

}

この例の指標はstackという名前です。

隠蔽ソートと可視ソート

メイヤー指標を定義するには、ソート記号の集合Sを2つの部分HとVに分ける必要があります。

S = H + V （共通部分がない和）

Hの要素を隠蔽ソート記号（hidden sort symbol）、Vの要素を可視ソート記号（visible sort symbol）と呼びます。インフォーマルには、隠蔽ソート記号は状態空間を表し、可視ソート記号は値の集合を表します。メイヤーによるCommand、Queryなどの区別はオペレーションの分類となります。オペレーション記号fのプロファイルにより分類します。s, t などは隠蔽ソート記号、a_i, b （添字のiは番号）などは可視ソート記号だとします。

prof(f) が s, a₁, ..., a_n -> s の形のとき、fをCommandと呼ぶ。
prof(f) が s, a₁, ..., a_n -> b の形のとき、fをQueryと呼ぶ。

他に、オブジェクトを生成するオペレーションがあります。

prof(f) が s, a₁, ..., a_n -> t の形のとき、fをCreatorと呼ぶ。

ソフトウェア的には、Commandは状態遷移を引き起こし、Creator（コンストラクター）は新しいオブジェクトを生成します。この違いは、オペレーション記号のプロファイルだけでは区別できません。例えば、s -> s という形のプロファイルを持つオペレーションが、状態遷移なのかクローニングなのか分からないですね。

そこで、キーワードoperationに代えて、query, command, creator を使い、意味的な区別をキーワードの違いで表現することにします。次はスタックの例です。Creatorを追加しています。



signature stack {

  hidden sorts : Stack;

  visible sorts : Value, Boolean, Error, OK;
  command push :: Stack, Value -> Stack;

  command pop :: Stack -> [Stack, (OK | Error)];

  query top :: Stack -> (Value | Error);

  query isEmpty :: Stack -> Boolean;

  creator new :: -> Stack;

  creator clone :: Stack -> Stack;

}

この指標stackは、Command, Query, Creatorから構成されているので、メイヤー指標と言ってもいいのですが、もう少し条件を付けることにします。

指標がメイヤー指標であるとは次のことだとします。

ソート記号が、隠蔽ソート記号と可視ソート記号に分かれている。
オペレーションは、Command, Query, Creatorのどれかである。
隠蔽ソート記号が1つだけ特定されている。それをsとする。
すべてオペレーションのプロファイルにおいて、左辺の最初の項がsである。

特定された隠蔽ソートsを主要ソート（記号）と呼ぶことにします。名前付き指標において、主要ソートを名前の直後に書いて、オペレーション宣言では主要ソートを省略することにします。スタックの例では次のようになります。



signature stack(Stack) {

  visible sorts : Value, Boolean, Error, OK;
  command push :: Value -> Stack;

  command pop :: -> [Stack, (OK | Error)];

  query top :: -> (Value | Error);

  query isEmpty :: -> Boolean;

  creator new :: -> Stack;

  creator clone :: -> Stack;

}

ここで、creator new はStackを参照しないので、別な指標に移すこともできます。



signature global() {

  hidden sorts : Stack;
  creator newStack :: -> Stack;

}
signature stack(Stack) {

  visible sorts : Value, Boolean, Error, OK;
  command push :: Value -> Stack;

  command pop :: -> [Stack, (OK | Error)];

  query top :: -> (Value | Error);

  query isEmpty :: -> Boolean;
  creator clone :: -> Stack;

}

上の例では、ソート記号は指標のなかで宣言されていますが、共通の名前を使っているので、指標の外でまとめて宣言したほうがいいでしょう。



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;

}

2つの指標に分割したほうが分かりやすいですが、単一の指標に直せることに注意してください。



signature {

  hidden sorts : Stack;

  visible sorts : Value, Boolean, Error, OK;
  creator global.newStack :: -> Stack;

  command stack.push :: Stack, Value -> Stack;

  command stack.pop :: Stack -> [Stack, (OK | Error)];

  query stack.top :: Stack -> (Value | Error);

  query stack.isEmpty :: Stack -> Boolean;

  creator stack.clone :: Stack -> Stack;

}

メイヤー指標の意味付けはどうする

メイヤー指標は、ソート記号の集合が隠蔽記号と可視記号に分割された多ソート指標で、オペレーションがCommand, Query, Creatorの3種に分類されているものです。メイヤー指標に意味（表示的な意味）を与えるとは、ソート記号とオペレーション記号に対して、なんらかの数学的な対象物を割り当てることです。

メイヤー指標の意味付けには幾つかの方法があるでしょうが、次のように考えるといいと思います。

可視ソート記号には、集合を割り当てる。例えば、記号'Boolean'には、集合 {true, false} を割り当てる。可視ソート記号は集合値定数として扱う。
メイヤー指標のCommandとQueryを取り出した指標（Creatorは除く）に対して、その指標に対するメイヤーオートマトンの圏を対応させる。
Creatorに関しては別に考える。

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