Edited at

Alloyを使って関係を学ぶ(9)

More than 1 year has passed since last update.


右分割

今度は任意の関係SとRについて共通のソースを持つ右分割 $ S / R $ という双対概念を定義できる.

これも普遍性による定義は置いておいて述語によるものを見ておく.

a(S/R)b \equiv (\forall c: aSc \Leftarrow bRc)

これをAlloyのコードにしてみる.

module RightDivision

sig A{
}

sig B{
}

sig C{
S: set A,
R: set B
}

fun rightDivSR[] : B -> A {
{b: B, a: A | all c : C { c in b.~R => c in a.~S}}
}
pred show{
some rightDivSR[]
}

run show

rightDivSRが $ S / R $ に相当する射で,二つの射をもらって一つの射を返す.

これは上の述語として解釈した右分割の定義におおよそそのまま対応している.

やはり方針としてはこれでグラフを表示させてどんなのが出てくるかを見てみたりrightDivSRをEvaluateしてみてどういう演算になるのかを調べてイメージ掴もうかなということです.


S / R はどんな関係か

まずはじゃんじゃんグラフを見てみる.

2017-05-28-063337_670x352_scrot.png

いきなり変なのが来た.

一旦無視してどういうものかは考えない.

2017-05-28-063345_670x352_scrot.png

2017-05-28-063354_670x352_scrot.png

2017-05-28-063407_670x352_scrot.png

左分割の双対ってことなのでなんとなく分かる気はする.

2017-05-28-063427_670x352_scrot.png

ムムム...

これはなぜB2からAへのrightDivSRという関係になりえないのか?

もう少し他も見ていく.

2017-05-28-063938_670x352_scrot.png

2017-05-28-064000_670x352_scrot.png

2017-05-28-064016_670x352_scrot.png

2017-05-28-064121_670x352_scrot.png

2017-05-28-064130_670x352_scrot.png

2017-05-28-064233_670x352_scrot.png

2017-05-28-064241_670x352_scrot.png

2017-05-28-064255_670x352_scrot.png

しばらく見ているとAが複数存在するケースが見たくなってくるね.

なかなか出現しないのでAlloyさんに

run show for 3 but exactly 2 A

と指示してみる.

2017-05-28-064758_670x352_scrot.png

2017-05-28-064822_670x352_scrot.png

2017-05-28-064829_670x352_scrot.png

2017-05-28-064855_670x352_scrot.png

2017-05-28-064911_670x352_scrot.png

2017-05-28-065002_670x352_scrot.png

2017-05-28-065015_670x352_scrot.png

2017-05-28-065045_670x352_scrot.png

2017-05-28-065111_670x352_scrot.png

2017-05-28-065118_670x352_scrot.png

2017-05-28-065147_670x352_scrot.png

2017-05-28-065158_670x352_scrot.png

2017-05-28-065235_670x352_scrot.png

2017-05-28-065252_670x352_scrot.png

2017-05-28-065308_670x352_scrot.png

2017-05-28-065328_670x352_scrot.png

2017-05-28-065337_670x352_scrot.png

つまり $ S / R $ というのは,Bの要素bに対してR関係にあるソースCの要素cの集まりcsがあったときに,そのcsが今度は関係SとしてAの要素aをターゲットに持つなら,そのbとaとの間の関係だ.

例えば


  • Bが冷蔵庫

  • Cが食材

  • Aが料理

として,


  • Rは食材Cが冷蔵庫Bに入っている関係

  • Sは料理Aを作るのに食材Cを使うという関係

とすると,rightDivSRはある冷蔵庫bから作れる料理という関係になる.

ただ,こっちの例だと冷蔵庫の中身が空っぽの場合がちょっと困るな.

あるいは


  • Bが教育課程

  • Cが科目

  • Aが学生

として


  • Rは教育課程Bは科目Cを含むよという関係

  • Sは学生Aが習得している科目Cという関係

とすると,rightDivSRは教育課程Bを学生Aが習得しているという関係か.

であれば科目が空の教育課程があったらどんな学生もその教育課程は習得している.

これならよさそう.

スッキリした.


捕捉

ちなみに前回の左分割と今回の右分割なんか本質的には同じじゃない?って思ったら正しい.

なぜなら関係は常に適切な逆を持つからで実際に

R \setminus S = (S^{\circ} / R^{\circ})^{\circ}

および

S / R = (R^{\circ} \setminus S^{\circ})^{\circ}

となるからだ.

比喩であれば大抵は能動態を受動態にすれば逆が取れてあとは矢印の向きを逆にして双対にすれば同じことだ.