Edited at

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

More than 1 year has passed since last update.


はじめに

AOP読んでる.

関数はともかく関係には免疫がないので吐きそう.

しばらく頓挫してたけどAlloy知ってこれなら試せるんじゃね?と思ったのでAlloyを武器に勉強再開してみる.

今回はまず基本からおさらい.


関数(あるいは全域関数)

型を集合と考えると,型A->Bなる関数とは任意のAの要素に対してBの要素がひとつ決まるような写像.

通常は関数といえば特にことわりがなければ全域関数(Total function)を指す.

つまりAの任意の要素aに対してBの要素bがひとつ決まる.

alloyで書くとこんな感じ.


TotalFunction.als

sig A {

f: one B -- oneは記述しなくても良い.defaultがone.
}
sig B{}

関数の例をいくつか挙げてもらおう.

2017-01-05-102803_498x352_scrot.png

2017-01-05-102842_498x352_scrot.png

2017-01-05-102915_498x352_scrot.png

2017-01-05-102921_498x352_scrot.png

いずれもAについては全域性(Totality)があることに注目.

蛇足だけど圏論なんかで集合の圏を考える場合にはこれらの図ひとつひとつが射1本に当る.


部分関数

全域性がない場合は部分関数(Partial function)という.

部分関数の場合にはAの任意の要素aに対してBの要素bが高々1つ決まる.


PartialFunction.als

sig A {

f: lone B
}
sig B{}

こいつの例もAlloyに挙げさせてみる.

ほとんどは全域関数の例と同じなので省略するとして,たまーに部分関数らしいのが出てくる.

2017-01-05-103155_498x352_scrot.png

2017-01-05-103113_498x352_scrot.png

これらはどんなBも対応しないようなAの要素aがある.

Haskellなんかで言えばundefinedがあるような関数でunsafeというプレフィクスが付けられることもあるがheadとかtailみたいにしれっと含まれてたりもする.

要するにキケンな関数だよ,キミ.

Agdaみたいな定理証明に使われる言語なんかには許されてない.

全域性が保証されてないと証明できたんだかどうなんだか分らないもんね.


関係

次は関係.

関数じゃなく関係ね.

関係になると型Aの任意の要素aに対してBの任意個の要素への対応が付けられる.

あるいはAとBの直積集合の部分集合として捉えることもできるし,その方が私はイメージしやすいかな.

Alloyで書くとこう.


Relation.als

sig A{

R: set B
}
sig B{}

本なんかだとaRbと書いてA->Bな関係を表現したりする.

やはりAlloyさんに例を挙げさせる.

2017-01-05-104236_498x352_scrot.png

2017-01-05-104312_498x352_scrot.png

2017-01-05-104321_498x352_scrot.png

2017-01-05-104334_498x352_scrot.png

2017-01-05-104341_498x352_scrot.png

とまぁ全域関数 < 部分関数 < 関係とどんどん一般的になっていくのが分かるかと.

AOPでは関数ではなく関係へと一般化する動機のひとつとして実数から複素数に進んだ時のように表現力が跳ね上がるんだと語っている.


合成

関数合成と同様に関係の合成(結合)も

R\cdot S

みたいに書く.

AlloyでもR.Sと書く.

ただしどっちが先でどっちが後かは注意が必要.

関係の結合はaRbかつbScなるbが存在するならa(R.S)cがあるようなもの.

ここは多分関数からの類推で結構直感的に理解できる.


包含関係

R\subseteq S

AlloyだとR in Sって書く.

関係をタプルの集合と考えるなら,集合の包含関係なので分かりやすい.


交わり

R\cap S

AlloyではR & Sと書く.

関係をタプルの集合と考えるなら,集合の共通部分になるので分かりやすい.


R^{\circ}

逆はAlloyだと~Rなどと書く.

これはAとBの関係Rをタプル(a,b)の集合だと見做すと,タプルの転置つまり(b,a)にあたる.

Alloyの図で言えば矢印が逆向きになるようなもの.

逆は逆関数みたいなのが関係へと一般化されたわけだ.


R.~R.RはRより大きいか?

Alloyを使ってるんで証明とまでは行かないけどスコープの範囲で反例ありや?とか図を確認しつつ関係について具体的に学ぶ.

やってみると自分の関係についての理解の浅さがあまりにも酷いのが自覚できる.

たとえば本を読んでると

R\subseteq R\cdot R^{\circ}\cdot R

みたいなのが出てくるんだが最初はどうも良く分からない.

包含関係の向きがどうもハテナ?ってなるんじゃないかと.

2017-01-05-112549_555x352_scrot.png

例えばこの図の例で考えると,Rはこの赤い線全部だ.

これをR.~R.Rで結合したからと言ってとくにこれ以上増えねーんじゃねーの?と思いがちじゃない?オレだけか?

2017-01-05-112706_728x352_scrot.png

Evaluatorを起動して確認してみるとR.~RってのはRで辿って~Rで逆向きに戻るときに関係が結合されて男\$0->男\$1みたいな関係が出来ている.

あーそっか.確かに.

つまりR.~R.Rってやると男\$0を出発点に見ると赤い線を3ステップで到達可能な範囲に関係の要素が拡張される.

男\$1から辿れる範囲についても同様だ.

なるほど...パンデミックこえぇ.

なお,これは


Theorem.als

assert TripleR{

R in R.~R.R
}
check TripleR

として確かに正しいってことを確認したりもした.

蛇足だけど,当然R.~R.RよりR.~R.R.~R.Rの方が大きい,さらにR.~R.R.~R.RよりR.~R.R.~R.R.~R.Rの方が大きい...となり以下同様にどんどん大きくなっていく.


おわりに

今回はここまでとして次回はモジュラ則なんぞをこねくり回してみたいと思います.

ちなみにモジュラ則はこれ.

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

もしかして剰余則と呼ぶの?

なにがどう剰余なのか知らんが.

ともあれ関係の圏とかアレゴリなんかを勉強してても正直定理の類が全然イメージ湧かなくて眠くなるのでAlloyさんに助けてもらいつつしばらく勉強を進めてみます.