関係圏、非決定性写像の圏、部分写像の圏とかに関する便利な記法

「関係を表す矢印の形をどうしようか？」で、関係圏の射を表す矢印の描き方をウンヌンしました。あれは、矢印をグラフィックスとして描く場合のことです。手書きやテキストエディタだと、複雑な形状は無理です。

それで、カラス足の矢印（下の図）を、もっと簡単に →* と表すことにしました。

アスタリスク記号「*」は、正規表現で0個以上の任意個を意味するわけで、なかなか都合がいいと思いました。しばらくこれを使っていたのですが、他の記法との関係（後述）で、 →# に変更しました。まー、これでもカラス足っぽいのじゃないのかなー。

単なる矢印 → は、集合圏の射、つまり普通の写像（＝全域単葉な関係）としました。部分写像、つまり全域とは限らない単葉な関係は、→? とします。再び正規表現とのアナロジーで言えば、値が0個または1個という意味でふさわしいかと。

関係圏と非決定性写像（集合値の写像）の圏は事実上同じものですが、定義は異なります。関係圏における射 R:A→B は、R⊆A×B ですが、非決定性の圏における射 f:A→B は、集合圏で f:A→Pow(B) のことです。Pow(B) はBのベキ集合です。関係圏と非決定性写像の圏を区別しなくてもいいときが多いですが、いちおう区別して繰り返しの記述も書いておきます。

さて、→#、→?、→ を使い分ける文脈で f:A →# B と書いたら次のどれかの意味です。

fは、関係圏で A→B という射である。
fは、非決定性写像の圏で A→B という射である。
fは、集合圏で A→Pow(B) という射である。

f:A →? B と書いたら次のどれかの意味です。

fは、関係圏で A→B という単葉な射である。
fは、非決定性写像の圏で A→B という単葉な射である。
fは、集合圏で A→B_⊥ という射である。
fは、部分写像の圏で A→B という射である。

B_⊥ は、B + {⊥} のことで、Maybeモナドをイメージすればいいでしょう。

そして、f:A → B と書いたら次のどれかの意味です。

fは、関係圏で A→B という全域単葉な射である。
fは、非決定性写像の圏で A→B という全域単葉な射である。
fは、集合圏で A→B という射である。
fは、部分写像の圏で A→B という全域な射である。

[A →# B] のように、外側をブラケットで囲んだら、「f:A →# B であるfの全体からなる集合」という意味だとします。Rel、ND、Set、Partial をそれぞれ、関係圏、非決定性写像の圏、集合圏、部分写像の圏だとして、次のようになります：

[A →# B] = Rel(A, B) = ND(A, B) = Set(A, Pow(B))
[A →? B] = Partial(A, B) = Set(A, B_⊥)
[A → B] = Set(A, B)

さらに、A# := Pow(A)、A? = A_⊥ という略記を導入します。この略記の都合で、「*」を「#」に変えました。A* だと「Aのリスト」の意味になるので。

今までの定義から、

[A →# B] = [A → B#]
[A →? B] = [A → B?]

という等式が成立します。「#」と「?」を移動するだけなので分かりやすいですね。また、関係圏のホムセットの定義から、

[A →# B] = (A×B)#

も成立します。

関係圏（非決定性写像の圏）のなかでは、直積に関してカリー化ができるので（「Alloyの矢印記法と、モノイド閉圏としての関係圏」参照）、次も成立します。

[A×B →# C] = [A →# B×C]

これだけの記法の工夫でも、だいぶ計算が楽になります。例題として、オートマトン（遷移系）の表現を扱ってみます。アルファベット（ラベルの集合）がAで状態空間がSであるオートマトン（ラベル付き遷移系）は、非決定性遷移写像 t:A×S→S で表現できます。tは非決定性なので、先の記法では t:A×S →# S と書けます。t':A → [A → S#] とか t'':S×S → A# なんて形でも表現できます。なぜならば：

  [A×S →# S]
= [S×A →# S]
= [S →# A×S]
= [S → (A×S)#]
= [S → [A →# S]]
= [S → [A → S#]]

  [A×S →# S]
= [S×A →# S]
= [S →# A×S]
= [S →# S×A]
= [S×S →# A]
= [S×S → A#]