Edited at

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

More than 1 year has passed since last update.


分割(Division)

共通のターゲットを持つ二つの射(関係)RとSが与えられたら左分割 $ R \setminus S $ を定義できる.

普遍性による定義は図式としては解り良いが意味が分からん.

左分割を述語で解釈すると,

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

だそうな.

これならalloyに翻訳できそうな.

といっても久々だったのでてこずった.

んで書いたコードがこちら.

module Division

sig A{
R: set B
}

sig B{
}

sig C{
S: set B,
X: set A
}
/*
pred leftDiv {
all b: B | some a: A, c: C | b in a.R implies b in c.S
}
*/
/*
pred leftDivRS [a: A, c: C]{
all b: B | b in a.R implies b in c.S
}
*/
fun leftDivRS[] : C -> A {
{c: C, a: A | all b : B { b in a.R => b in c.S}}
}
-- {c: C | all b : B { b in c.S}}
-- {a: A| all b: B { b in a.R}}

pred show{
-- leftDivRS[] = C -> A
some leftDivRS[]
-- no leftDivRS[]
-- some (C -> A) - leftDivRS[]
-- some leftDivRS[] - (C -> A)
-- 半可換?
-- some S - leftDivRS.R
-- 可換?
-- no S - leftDivRS.R
}

run show

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

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

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


R \ S はどんな関係か?

とりあえずグラフを表示させてみてガンガン眺めていく.

2017-05-27-113752_670x352_scrot.png

2017-05-27-113803_670x352_scrot.png

2017-05-27-113811_670x352_scrot.png

2017-05-27-113822_670x352_scrot.png

2017-05-27-113838_670x352_scrot.png

2017-05-27-113903_670x352_scrot.png

このあたりまで見るとおよそ分かった気にはなるが,もう少し見てみる.

2017-05-27-113917_670x352_scrot.png

おっと,これも含まれる.

2017-05-27-113952_670x352_scrot.png

2017-05-27-114003_670x352_scrot.png

2017-05-27-114026_670x352_scrot.png

述語での表現における"任意の"の意味を取り違えてたような気もする.

本当に正しいAlloy式になってるのかなという不安もあるが.

2017-05-27-114242_728x352_scrot.png

2017-05-27-114307_728x352_scrot.png

2017-05-27-114329_728x352_scrot.png

2017-05-27-114414_728x352_scrot.png

2017-05-27-114451_728x352_scrot.png

2017-05-27-114517_728x352_scrot.png

2017-05-27-114632_728x352_scrot.png

2017-05-27-114644_728x352_scrot.png

2017-05-27-114658_728x352_scrot.png

2017-05-27-115009_728x352_scrot.png

2017-05-27-115411_728x352_scrot.png

2017-05-27-115431_728x352_scrot.png

2017-05-27-115443_728x352_scrot.png

2017-05-27-115511_728x352_scrot.png

2017-05-27-115945_728x352_scrot.png

2017-05-27-120029_728x352_scrot.png

2017-05-27-120057_728x352_scrot.png

ここまででほぼ概念は捉えられたように思う.

つまりこうだ.

$ R \setminus S $ というのはあるAの要素aがR関係を持つBの要素b全てに対してS関係を持つようなCの要素cがあるとして,aとcの間の関係がそうだ.

例えば,


  • Bを住所

  • Aを市

  • Cを県

だとする.


  • Rは住所bが市aに含まれる

  • Sは住所bが県cに含まれる

だとすると $ R \setminus S $ というのは住所が市に含まれるなら県に含まれる,つまり $ a(R \setminus S)c $ はa市はc県に含まれる.

あるいは


  • Bを駅

  • Aを路線

  • Cを鉄っちゃん

として


  • Rを駅bは路線a上にある

  • Sを鉄っちゃんbは駅cに降り立ったことがある

だとすると $ R \setminus S $ というのは駅が路線上にあるなら鉄っちゃんは駅に降り立ったことがある,つまり $ a(R \setminus S)c $ は路線aを鉄っちゃんcは制覇した.

そういう感じかな.

2017-05-27-120539_728x352_scrot.png

おっとこうなるのか...

2017-05-27-120627_728x352_scrot.png

2017-05-27-120646_728x352_scrot.png

2017-05-27-121514_728x352_scrot.png

なるほど,住所と言えるような場所がない市や駅が無いような路線はあらゆる県に含まれたりどんな鉄っちゃんも制覇したことになる.


右分割

これの双対になるのかな?

つづいて右分割だけど一旦切ることにする.

続きは次回.