Alloy で形式手法を始めてみた！～集合の演算・発展編～
ここでは，集合に対する発展的な演算を説明します．
集合と関係式の演算
集合と関係式の演算には，ドットジョインがあります．
ドットジョイン
Alloy では，集合と関係式，あるいは関係式同士に定義される，ドットジョインという演算子があります．
Java や C# では，あるクラスのオブジェクトの public なメンバにアクセスするには object.member のようにドットを使ってメンバを指定しますが，Alloy のドットジョインはそれとは似て非なるものです．
イメージとしては，RDB における JOIN に近いです．
以下，r = {(a, b), (a, c), (b, d), (c, d)}, A = {a, b}, D = {d} とします．
このとき，ドットジョイン A.r は以下のような演算になります．
つまり，集合 A の要素を先頭に持つ関係式を選び，キーとなった要素を落としたもののことです．
同様に，ドットジョイン r.B は以下のようになります．
要素と関係式の演算
要素と関係式の演算には，ボックスジョインがあります．
ボックスジョイン
要素 e と関係式 r に対し，r[e] を e.r と定義します．ここで，単一の要素 e は，唯一の元 e をもつ集合 {e} とみなされています．
これにより，例えば関係式 r の第一成分に重複がない場合，r を関数または部分関数とみなして r[e] という関数的な表示が可能になります．
関係式と関係式の演算
関係式と関係式の演算にもドットジョインが定義できます．
ドットジョイン
r1 = {(a, b), (a, c), (b, c)}, r2 = {(a, c, d), (b, d, e)} の場合，r1.r2 を以下のように定義します．
このとき，r1.r2 は以下のようになります．
つまり，r1 の最後の成分と r2 の最初の成分が一致するものを，キーになった要素を落としてつなげたもののことです．
二項関係に対する演算
二項関係に対する演算には，転置（~），推移閉包（^），反射的推移閉包（*）があります．
二項関係とは，各要素が (a, b) のように二つの要素のペアになっているような集合を指します．
転置（~）
関係式の各要素を逆順に並べ替えたものです．
r = {(a, b), (b, c)} とすると，~r = {(b, a), (c, b)} となります．
推移閉包（^）
推移閉包とは，二項関係を何度か適用して到達可能なペア全体の集合のことです．
例えば，r = {(a, b), (a, c), (b, d)} とすると，この二項関係だけでは a から d へ到達できませんが，
(a, b) と (b, d) の二つを使えば，つまり，{(a, b)}.{(b, d)} = {(a, d)} により，(a, d) という要素が得られ，a から d まで到達可能であることがわかります．
図で表すと，以下のようになります．
- a から到達可能なのは b, c, d なので，(a, b), (a, c), (a, d) が ^r に入ります．
- b から到達可能なのは d なので，(b, d) が ^r に入ります．
- c, d から到達可能な点はありません．
よって，^r = {(a, b), (a, c), (a, d), (b, c)} となります．
言い換えると，ドットジョインを何度か使って到達できれば良いわけですから，
^r = r + r.r + (r.r).r + … となります．
反射的推移閉包（*）
これは，推移閉包に加えて自分自身との関係式を追加したものです．
先程の例だと，^r + {(a, a), (b, b), (c, c), (d, d)} となります．
言い換えると，*r = ^r + iden となります．
関係式の制限
始集合の制限（<:）
集合 A と関係 r に対し，A <: r で，r の第一成分を集合 A に制限したものを表します．
終集合の制限（:>）
集合 B と関係 r に対し，r :> B で，r の最後の成分を集合 B に制限したものを表します．
始集合と終集合の制限をまとめると，以下のようになります．
抽象シグネチャ Airport は，Airport 同士の関係式として route を持つとします．ここでは，route は，空港間に直行便の航空路があるかどうかを意味することとします．
また，Airport は国際空港（羽田や関空など）か国内便しか飛ばない空港（伊丹や丘珠など）かのどちらかであるとします．
abstract sig Airport {
route: set Airport
}
sig InternationalAirport, DomesticAirport extends Airport {}このとき，DomesticAirport <: route :> InternationalAirport は，国内先しか飛ばない空港から国際空港への航路を表します．このように書くと，記法が理解しやすいのではないでしょうか．
関係式のオーバーライド（++）
r1, r2 はともに要素のタプルの長さ（アリティ）が同じであるような関係式とします．
このとき，r1 ++ r2 を，以下のように定義します．
- r2 の要素全てと，r1 の要素のうち r2 の要素の第一成分を第一成分にもつもの以外の和
文字にするとわかりにくいですが，図にすると以下のようになり，オーバーライド感が出ます．
最後に
次は，if や iff などの条件式，制約条件の書き方や，Pred, Func, Fact などについてまとめたいと思います．
参考
非公式ドキュメントですが，基本的にはここを参照しています．
公式の言語リファレンスも参考にしています．
過去の投稿
- Alloy で形式手法を始めてみた！～導入編～
- Alloy で形式手法を始めてみた！～シグネチャ編～
- Alloy で形式手法を始めてみた！～関係式の多重度編～
- Alloy で形式手法を始めてみた！～特殊なシグネチャ編～
- Alloy で形式手法を始めてみた！～集合の演算と数値編～
では！
コメント