SimpleとEntireな射

Simpleな射というのは, $S:A\leftarrow B$

S\cdot S^{\circ}\subseteq id_{A}

なる射のこと.

一方,Entireな射というのは,$R: A\leftarrow B$

id_{B}\subseteq R^{\circ}\cdot R

なる射のこと.

alloyで書くと,

module SimleEntire


sig A{

}

sig B{

    S: set A

}

fun id_A : A -> A{

    A -> A & iden

}

fun id_B: B -> B{

    B -> B & iden

}

pred Simple{

    ~S.S in id_A

}

pred Entire{

    id_B in S.~S

}

pred show{

    Simple[]

}

run show

Simpleな射を見てみる

これで述語showの中でSimple[]しているので例を挙げさせるとSimpleな射が見れる.

Simpleの定義を見ると, $S\cdot S^{\circ}\subseteq iden$であるからして,図ではBからAに向かって矢印が伸びているけど,逆向きつまりAからBへ行って再びAへ戻ってくるように線をたどる(結合する)とAからAへの関係になる.

そのとき自分自身への関係だけ,その範囲内に収まるよというのがSimple.

このような結合が自分を含みうるのは当然だとして,ポイントはA0 -> A1みたいにAの中の異なる要素間の関係が生まれることはないようなそんな状況にしているのがこの条件.

ではこの結合$S\cdot S^{\circ}$によってA0 -> A1みたいなのが生まれるのはどんな状況かというとそれは,あるBの要素から複数のAへの関係があるようなものだ.

つまりこういうやつ.

この図では合成によってA0からBへ行ってBからA1へ行くような経路ができるので,$S\cdot S^{\circ}$にはA0 -> A1やもちろんA1 -> A0も含まれることになる.

これではidenの部分集合($\subseteq$)とは言えなくなるのでアウトだ.

ということでSimpleな射というのは,Bから複数のAへの関係がないようなものだ.

Bを男,Aを女としてSという矢印で表される関係を「BかAに言い寄っている」とするとSimpleな射では気の多い男というのは居ないのがSimpleだ.

ちなみに独身男も見て取れるが言い寄ってても一途なのがこの射の特徴.

言い寄ったりしないのが草食系だとすれば草食系と一途な男しかいない.

これは部分関数にあたる.

Entireな射を見てみる

述語showの中を書き換えてEntire[]して例を挙げさせるとEntireな射が見れる.

こちらはSimpleの例でいうところの一途なやつはいるけど草食系は不在.

逆に草食系の代わりに肉食系(複数の女に言い寄るやつ)が居る.

いずれにせよ独身男はいないので全域的(つまりどのBも少なくともひとつAがある)な関係だといえる.

SimpleでEntireな射

次のように書き換えればSimpleかつEntireな射になる.

pred show{

    Simple[]

    Entire[]

}

これもalloyに例を出させて見てみる.

これは関数にあたる.

より正確には全域関数なのでSimpleなのとは違う.

すべての男はただ一人の女に言い寄っているので一途な奴ばっかりの世界.

まとめ

前回の時には間違えてた.

Simpleは単射でEntireは全射みたいなものだと書いたけど,単射というのとは違うな.

SimpleかEntireかSimpleかつEntireかは部分関数か関係か全域関数かに対応しそうだ.

次回はもう少しこのSimpleとEntireについてみるつもりだけど,気が変わってTabularをやるかもしれないしやらないかもしれない.

正直理解が浅すぎるので書けそうなことがあればそれをテーマにやる.