AOP
AlloyAnalyzer
algebra
relational

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

More than 1 year has passed since last update.


まえおき

ちょっと間があいてしまった.

AOPのお勉強です.

議論の展開についていけないのはどうも包含の式変形が直観的に理解出来てないからだろうと思う.

$R . R^{\circ}$とかが$id$より大きくなるのとかはもう分かるんだけどでももどかしい感じはやっぱりまだある.

論証を追いかけてて気付いたのはおそらくその辺りの理解が不足しているからだと思われる.

復習を兼ねて少し戻って包含関係にまつわるものを少し掘り返してみる.


交わりの上の結合の半分配則

まずアレゴリの基本演算のひとつ交わりなんだが,こいつを使うと単調性の公理を2つの包含で言い直すことができるという話で出てくるのがこれ.

 R . (S \cap T) \subseteq (R . S) \cap (R . T)

 (R \cap S) . T \subseteq (R . T) \cap (S . T)

分配すると$\subseteq$という不等式になる.

というのがなかなか最初納得しにくい.

とりあえず例を出す.


Alloyで事例作成

図を書くのにはAlloyを使います.

sig A {

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

pred show{
some (R.S & R.T) - R.(S & T)
}

run show for 3 but exactly 1 A, 3 B, 2 C

showで$R.(S \cap T) \subseteq (R . S) \cap (R .T)$において右辺の方が左辺より大きくなるケースを含むものに限定して探させていますが,一度は自分で考えた方が良いかもね.1

これでExecuteしてinstanceを見る.2017-05-12-094652_613x352_scrot.png

これで説明すると,$R.(S \cap T)$はないんですが,$(R.S) \cap (R.T)$となるとA -> C0という関係があるわけです.

不等式になります.

一応Alloyで確認したければ

2017-05-12-095325_613x352_scrot.png

こんな風にEvaluator立ち上げて確認してください.

もう一方の不等式のためのAlloyのコードです.

sig A {

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

pred show{
some (R.T & S.T) - (R & S).T
}

run show for 1 but exactly 1 A, 3 B, 2 C

これで例を出させます.

2017-05-12-095646_613x352_scrot.png

分かる通り,$(R \cap S).T$はありませんが,$R.T \cap S.T$はA -> C1という関係があります.

やはり不等式になっていますね.

Evaluatorでも確認できます.

2017-05-12-100050_613x352_scrot.png


直感的に理解したい

さてと,これはこれで別に何の異論もなくて良いんですけどね.

個人的には関数からの拡張として関係を見ていたのでどうもイメージが関数由来になっててこれが理屈では分かるんだけど自在に不等式を駆使した論証ができない.

等式じゃなく不等式になるってのが考えれば気付くけど直感的に不等式になるだろって思えない.

こうしたほげほげ則のようなものをあるのかどうかも分からずに探しまわって参照しながらではとても実用にならないと考えました.

もっと自分の言葉になるところまでいかないと到底使えないなと.

まずはこれらの関係をもう少し親しみのあるものにして考えてみます.


車と釣り道具を貸してくれ

週末に釣りに行きたいなと思ったとします.でも車も釣り道具もない.

で知り合いからそれらを借用して行こう!とポジティブに思ったとします.


  • Rを知人関係とします.

  • Sが車の所有関係とします.(持っていれば貸すのは拒まずとします)

  • Tは釣り道具の所有関係とします.(持っていれば貸すのは拒まずとします)

$R.(S \cap T)$はつまり知人で車と釣り道具を持っている人を探してその人から両方ともゲット2って筋書ですね.

一方$(R.S) \cap (R.T)$は知人で車持ってる人から車を借りて知人で釣り道具を持ってる人から釣り道具を借りてそれぞれからゲットだぜって筋書ですね.

これ明らかに後者の方が選択の幅というか可能性が見えてきます.

この選択の幅の広さというか可能性の高さというのがまさに関係という直積集合の要素の数の多さを物語っている.

これが最初の不等式でしょうね.


愛情と金が欲しい

次はもっと欲望炸裂.

愛のある相手と付きあえれば楽しいでしょう.

でもやっぱりお金も大事.

どんなにイケメンでもお金がないと...


  • Rは愛情関係とします.(AはBを愛してる)

  • Sは便利関係(?)とします.(AはBをオサイフクンと見ている)

  • Tが余力(時間)があるかどうかとでもします.(時間があれば来るもの拒まずとします)

$(R \cap S).T$はイケメンで金持ちというサイコーの相手と付きあえるんですがそもそも探す時点でなかなかハードルが高そうです.

さらに増やして三高というのが昔話なんかに登場しますが,多分今は絶滅危惧種.

一方で$R.T \cap S.T$はというとイケメンをゲットしつつさらにお金持ちもゲットしちゃう3というややビッチな感じですけど実現の可能性がグッと高くなるはずです.4


まとめ

こう考えると述語論理っぽく解釈するとなんか理解しやすそうに思います.

というかそもそも記号がそう読めと言ってることにあらためて気付かされたというだけですが.

で読み換えですが,$\cap$はそのまんま連言ですね.

実は合成の$.$も連言とみなしてだいたい良さそう5なんですが,違いはソースとターゲットの組み合わせが違うってところです.6

$R \cap S$の場合には$R$と$S$は同じソースとターゲットを持ちますが,$R.S$は$R$のソースと$S$のターゲットが同じものだとかね.

つまり連言といっても乗ってくる文脈が微妙に違うということかな.

ただその文脈って無意識に折り込んでたりしてあんまり気にならなかったりするから,そこはちょっと頭の片隅にでも置いておけば良いくらいでしょうか.

「車と釣り道具を持つ人と知りあっている」より「車を持っている人と知り合いでありながら釣り道具を持っている人とも知り合いである」方が広いってのは深く考えるようなものでもなく直感的に分かると思います.

「自分を相手にしてくれるイケメンで金持ちを掴まえる」可能性より「自分を相手にしてくれるイケメンと自分を相手にしてくれる金持ちを両方掴まえる」方が可能性が広いってのも直観的に分かるかるんじゃないかと思います.

とりあえず私が自分で分かった気になったので,とりあえずメモ書きということで記録しておきます.





  1. たとえばrunでsigの要素数を狙い打ちしてますけど,それも自分で事例を手元で考えてその最小限の例を出させるようにしているためです. 



  2. グラフで到達可能なパスがあるのでゲットだぜ!って気分です. 



  3. 同じく彼の余力(時間)に到達可能なパスがあるとゲットだぜ! 



  4. ここで言う実現の可能性ってのは条件を満たすようなパスはどちらがより潤沢にあるはずかという話です.念の為. 



  5. 実際にAOPでもRELでのモジュラ則の証明をしてたりするとどちらも連言. 



  6. 結合は一応別物だけど直積と制限の組み合わせで制限演算の方が連言ぽいので区別があるはずですがまぁ細かいことはええがな...