AOP
AlloyAnalyzer
algebra
relational

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


分割の半可換

以前Alloyを使って関係を学ぶ(8)Alloyを使って関係を学ぶ(9)でそれぞれ左分割と右分割を考えたんですが,どうも半可換になるところがよく分かってなかったので調べていました.

そうするといろいろ理解が浅すぎたなと思う部分が出てきたので再度そのあたりをまとめます.


左分割

まずは定義から再掲.

a(R \setminus S) c \equiv (\forall b : bRa \Rightarrow bSc)

これは$R\setminus{S}$関係があるなら右辺にあるとおりの述語が成り立つし、右辺の術語が成り立つなら$R\setminus{S}$関係があるということ.

早速具体例を示す。

AlloyのコードはAlloyを使って関係を学ぶ(8)の通り.

2018-02-23-051928_786x352_scrot.png

この関係はもちろん半可換だ。

$R\cdot{X}\subseteq{S}$ になっていて$C\mapsto{B1}$ があるからS関係の方が大きい.

さて,もしこの順序関係を無理矢理逆にしようとしたらどうなるか?

つまりR関係の要素のひとつとして$A\mapsto{B0}$があったとしたらどうなるかを想像する.

もしあれば確かに $C\mapsto{B0}$ができるのでSからはみ出してしまう.

だがもしそうなってたらそもそもCとAとの間には左分割の関係は成立しえない.

というのが左分割の定義の言っているところ.

AとR関係にあるような任意のBに対してS関係にあるようなCとの間の関係なので,もしB0との間にS関係がないならそんなCとの間には$R\setminus{S}$関係もないのだ.

実は以前の記事を書いたときにはこのあたりが良く分かってなかった.

というわけで $R\cdot{X}\subseteq{S}$ となるのは分った.

$R\setminus{S}$はそういうXの中で最大のものなんだけど,それは最初の定義において右辺が成り立つなら$R\setminus{S}$関係もあることになるという右辺から左辺への含意があることに由来している.

ああナットク.

というわけでこの$R\setminus{S}$というAとCとの関係をSの下でRという表現のニュアンスもちょっと分かった.

もし上の具体例で$A\mapsto{B0}$があればAとCとの間には$R\setminus{S}$関係はなくなるので,AとCとはSの下でRとはならないよなぁと.

一方,上の具体例で$A\mapsto{B1}$がなくても良い点も注意.

Sの下でRってのはRがあるならSもなきゃならないんであって,RがないならSはあってもなくてもどうでもいいから.


右分割

右分割は左分割と似てて対合を取れば逆変換できるから同じようなもんと思ってたんだけど,どっこいこっちも理解が浅すぎた.

こちらは左分割なんかよりずっと難しかったかも.

やはり定義を再掲しておく.

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

$S/R$関係とはbとR関係にあるような任意のcがS関係にあるようなaとの間にあるような関係.

逆に右辺が成り立つようなaとbとの間には$S/R$関係があることになる.

まず最初の例.

2018-02-23-100027_728x529_scrot.png

これは確かに満している.

そもそもBに対してR関係にあるようなCが一切ないので右辺の述語がどんなAに対しても成立しちゃうから.

つまりR関係がないようなBはあらゆるAとの間に$S/R$関係がある(なくてはならない).

2018-02-23-100157_728x529_scrot.png

ほら,数が増えてもこの通り.

じゃあ次の例.

2018-02-23-100208_728x529_scrot.png

左のは良いとして右の$C\mapsto{B1}$はどうか.

B1からA0やA1に$S/R$関係がないの分かるかな.

これはB1に対してR関係のあるCが存在しているのだが,そのCがS関係にあるようなAが無いので今度は右辺がどんなaに対しても不成立になるから.

そうか...

さて次の例はちょっとすぐには分からなかった.

2018-02-23-100716_728x529_scrot.png

問題その1.

B2からA1への$S/R$関係がないのはなぜか?

(C1とB0あるいはB1とA0との関係と似ているのに)

問題その2.

B2からA0への$S/R$関係がないのはなぜか?

(似たような立ち場のB0やB1にはあるのに)

ポクポクポクチーン.

では答合わせ.

回答1.

B2に対してR関係にあるのはC0とC1の2つ.

C0は確かにA1との間にS関係があるんだが,C1はない.

$S/R$関係の定義によればR関係にある任意のCがS関係にあるAのと間にあるような関係なので,これが満されてないから.

つまりRならSだってことが演繹可能じゃないとダメ.

回答2.

回答1と同じ理由による.

$B2\mapsto{A0}$関係が存在するためにはB2とR関係にある任意のCがA0とS関係にないといけない.

C1は確かにA0とS関係にあるが今度はC0がA0とS関係にないからだ.

もう1例.

2018-02-23-100740_728x529_scrot.png

この図で$B1\mapsto{A0}$の関係がないのはなぜか?

もちろん$C0\mapsto{A0}$となるS関係がないからだ.

というわけでAとBとの間の$S/R$関係つまりRの上でSというのはRがあるんならその前提の上でSもあるような関係と読めそう.


右分割の半可換

さて半可換な関係はこうだ.

X\cdot{R}\subseteq{S}

例えば直前の図で確認すると確かに半可換だ.

$X\cdot{R}$には$C1\mapsto{A0}$は含まれないがSには含まれている.

もし$B1\mapsto{A0}$が$S/R$関係として存在してればSより大きな要素($C0\mapsto{A1}$)を持つことになるが,

そうなったらそもそもそれは$S/R$関係の定義の右辺を満さない.

やはり定義からこの順序関係は強制されそうだ.

そしてそのようなXの中で最大のものが$S/R$関係だというのも左分割の時と同じで右辺が成立するならAとBとの間には$S/R$関係があるという右辺から左辺への含意があるから.


まとめ

半可換の順序関係の向きはそれぞれの分割の定義にある述語から決まる.

そして各分割がそういう関係の中で最大というのを保証するのはその述語が成り立つなら分割関係があるという右辺から左辺への含意があるため.

もしその含意がなければX関係を間引くことでより小さな関係は作れる.


おわりに

たとえば右分割であればXとして$S/R$以外にも考えられる関係はあるが,$X\cdot{R}\subseteq{S}$を満すようなXのうち最大のものという定義の仕方も$a(S/R)b \equiv (\forall c: aSc \Leftarrow bRc)$という定義の仕方でもどちらでも同じことであるという話なんだが,そのあたりはやはりキチンと証明しないとにわかには...

そもそも分割という関係の言わんとするところがあまり理解できてなかったようなので,イメージが具体的に持てるようになったところで今回はおしまい.