AOP
AlloyAnalyzer
algebra
relational

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

More than 1 year has passed since last update.


モジュラ則

まずはモジュラ則から.

R\cdot S\cap T\subseteq R\cdot(S\cap R^{\circ}\cdot T)

コイツです.

AOPでは包含関係と合成そして交わりを関係付けるアレゴリの公理として登場します.

デデキントのモジュラ則(Dedekind's rule)としても知られる.

モジュラ則は交わりの上の合成についての分配則の弱いやつ(弱いというのは等式ほど強く言えないからそう言うぽい).

まぁ右辺を見ると分配則っぽさはワカル.


成り立つことを確認

まずはalloyでコード書いてみてモジュラ則がそもそも成り立ちそうなことを確認します.


Allegory.als

module Allegory

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

-- モジュラ則
assert ModularLaw {
R.S & T in R.(S & ~R.T)
}
check ModularLaw

pred show {}
run show


これExecuteすると反例ナッシング!って言ってくれるのでまぁ正しそう.

checkコマンドのスコープを10まで上げても問題ない.


モジュラ則とは

そもそもモジュラ則ってなんでしょうか?

ひとまず図を見てみます.

2017-01-05-164952_440x529_scrot.png

ここでCを男の子グループとします.

Bは女の子グループ.そしてAは女の子の特定の一人A子ちゃんとします.

線は全て友達関係とします.RもSもTも全部です.

あと矢印になってるけど向きも基本的に関係ないです.

結合する時には勿論関係あるけどどっち向きでも両者が友達だと見做します.

例えばこの図ではC2くんはB0,B1ちゃん達とは友達ですがA子ちゃんとは友達ではありません.

C0くんはB1,B2ちゃんとA子ちゃんと友達です.

彼は男子におけるキーパーソンです.

A子ちゃんの同性の友達はB0とB1ちゃんになりますね.

B1ちゃんは女子のキーパーソンです.

というのも,このB1ちゃんはA子ちゃんと直接の友達で,しかもC0くんというA子ちゃんとも友達でかつA子ちゃんと共通の女友達(B1ちゃん自身)も居るからです.

まぁ言ってしまえば,女子のB1と男子のC0がキモです.

モジュラ則はこうです.


まず右辺も左辺もC->Aなので男子からA子への経路を問題にします.

左辺は男子の中で,直接Aと友達で,かつ,A子の女友達とも友達なヤツ.

右辺については一旦女子に注目します.女子の中で直接Aと友達で,かつA子の男友達とも友達な子をキーパーソンとします.右辺全体としてはそのキーパーソンと友達な男子です.


一応ことわっておくと,この図の例の場合にはAはひとつしかないのでC->Aは実質A子ちゃん固定したものと同一視して勝手にCつまり男子の集合と読み換えてしまっていますが,正確には男子からA子への経路が両辺の対象です.

ポイントは左辺つまり(R.S & T)のメンバであるC0は当然右辺にも含まれるということ.

C0-B1-AとC0-Aのこのふたつの経路だけに注目します.

するとC0を起点に見れば左辺を満足します.

一方でB1起点で見れば~R.Tという経路はまさにB1->C2->Aの経路にあたり,単に起点を変更しただけにすぎないからB1はS & ~R.Tを満す女子だと言えます.

さらにC0->B1であるRを合成してR.(S & ~R.T)はC2->Aへの経路を作ります.

C0はB1がキーパーソンとなるためのキーパーソンと言えます.(逆もそうかもしれません.)

一方C2くんは違います.

彼はA子とは直接の友達ではないので左辺には含まれませんが,B1の友達であるC0くんを介してA子ちゃんと繋りを持てることで右辺に入ってきます.

C1くんは残念ながらキーパーソンであるB1と繋りを持てないため,つまりB1と友達ではないため右辺にも入ってこれません.

というわけでモジュラ則を再度眺めると,


左辺は男子のうち,A子と直の友達でA子の女友達(X)とも友達なヤツ

右辺は男子のうち,左辺における(X)なるキーパーソンと友達なヤツ

当然左辺の男子はXと友達なので右辺にも含まれるから左辺より右辺の方が大きい.


こんな感じか.

ただし,Xは単にA子の女友達ではなく左辺の男子と友達であるというところまで含めて求められるので念の為.


分配則はどうなる?

モジュラ則は交わりの上の合成についての分配則にも見えますがやや違います.

では分配則はどうなっているか?

R\cdot(S\cap R^{\circ}\cdot T) \subseteq R\cdot S\cap R\cdot R^{\circ}\cdot T

等号ではなく包含関係であることに注意.

実際ここまで広げると,この右辺にはさっきは含まれてなかったC1が含まれるようになります.

C1はR.SについてはC1->B0->Aの経路があり,R.~R.Tの経路についてはC1->B2->C0->Aがあるからです.

R.~RするとC1から2ステップで到達可能な男子の友人を含めることによって友人関係を拡張できるからですね.

さっきC1がモジュラ則の右辺に含まれなかったのは右辺がキーパーソンB1と友達であることを要求したからです.

というわけでモジュラ則と分配則をくっつけるとこんな感じでまとめ.

R\cdot S\cap T\subseteq R\cdot(S\cap R^{\circ}\cdot T))\subseteq R\cdot S\cap R\cdot R^{\circ}\cdot T


おわりに

というわけでモジュラ則を調べました.

多少イメージは出来てきましたが,分配則なんかでもそうですけど式変形がキビしいです.

alloy使ってサンプルを図示してEvaluatorで試したりassertionを噛ましてようやく判ったような...という程度でやっぱり良く解りませんでした.

なんだよモジュラ則のモジュラって...

とりあえず慣れも必要だと思うんでまだしばらくは頑張って続けます.

次回は射(ここでは関係)の性質各種登場します.

対称的とか反対称的とか余反射的とかそういうの.