Edited at

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

More than 1 year has passed since last update.


射の特性もろもろ

今回は射,ここでは関係ですが,の特性とされるものを調べます.

登場するのは以下です.


  1. 反射的(reflexive)

  2. 推移的(transitive)

  3. 前順序(preorder)

  4. 対称的(symmetric)

  5. 反対称的(anti-symmetric)

  6. 同値(equivalence)

  7. 半順序(partial order)

  8. 余反射的(coreflexive)

今回は淡々と眺めていきますが,これらはアレゴリに登場する関係の性質について言うものです.

例えば,「余反射的な射の場合であれば...」とか「ここで射が推移的なら...」みたいな感じで使われます.

つまり任意の関係が持つ性質とか定理ではなく,関係のクラスのようなものです.

念の為に確認しておきますが,射つまりここでは関係ですが,alloyでインスタンスを出したときに表示される図のひとつひとつが1本の射と見ます.

つまり関係はタプルの集合で表現していて,この集合ひとつが図示されているので,それが1本の射です.

なので圏論の文脈に移して考えたら,これらの性質はあくまで1本の射の性質を言っているものです.

なのでここのサブタイトルも「射の特性」なんですね.

問題はAとBの関係というと単にAとBの直積集合の部分集合のイメージしか(私には)なく,反射的な射(関係)ってのはどういう構造の関係を言うのかみたいな具体的イメージがないことです.

そうするとやっぱり「反射的だから」とか言われて論理を展開されても困っちゃうんですよね.

というわけで今回はalloyで図式を眺めてその見た目の特徴を把握して慣れていこうぜっていう主旨です.

AOPにも話の流れ上,これがひととおり説明されていますし.


Alloyコード

とりあえず最初にコードを晒します.


Properties.als

module Properties

sig A{
R: set A
}

pred Reflexive{
iden in R
}

pred NonReflexive{
iden not in R
}

pred Transitive{
R.R in R
}

pred NonTransitive{
R in R.R and R != R.R
}

pred Preorder{
Reflexive[] and Transitive[]
}

pred Symmetric{
R in ~R
}

pred NonSymmtetric{
R not in ~R
}

pred AntiSymmetric{
R & ~R in iden
}

pred Equivalence{
Symmetric[] and Preorder[]
}

pred Partialorder{
AntiSymmetric[] and Preorder[]
}

pred Coreflexive{
R in iden
}

pred show{
Reflexive[]
}
run show


このコードのshow述語には今 Reflexive[] とだけ書いてありますが,ここを書き換えてインスタンスを見ることで以降進めていきます.


反射的(reflexive)

pred show{

Reflexive[]
}

で見てきます.

異なる要素間の関係はどうでも良い.あっても無くても双方向にあってもどうでも良い.

重要なのは全ての要素に自身への関係があること.

$id\in R$だから.

つまり反射的(reflexive)な射(関係)というのは,仮にその関係をほげ関係とするなら「どんな要素を取っても自分は自分とほげ関係にある」と言えるような関係のこと.

念のため反射的ではないものも見ておく.

pred show{

NonReflexive[]
}

としてAlloyさんに例を出してもらう.

というわけで反射的な要素があっても良いけど,反射的でない要素がひとつでもあれば反射的な射とは言えない.

反射的な射だと言ったら,その時点でどんな要素も自身へ向かう写像があると思って良い.


推移的(transitive)

pred show{

Transitive[]
}

で見てきます.

閉じているということか.

$R\cdot R\in R$だけど,これは$R\cdot R$というのはこの赤い矢印を2ステップ繋いだ矢印.

これが元々の$R$にあるということ.

結合($\cdot$)は常に可能だが,その結合の結果出来る関係が元の$R$にそもそも含まれている.

つまり$R$の図の中に存在する赤い線で出尽くしている関係.

例えば「xはyの祖先である」というのを$xRy$という関係とすれば(ただし自身は自身の祖先であるというのも認めるとする)と推移的な関係だと言える.

祖先の祖先は祖先なのでxがyの祖先でyがzの祖先ならxはzの祖先だよねってことで$R$にはそもそも含まれるから.

逆に言えば結合によって新しい写像というかタプル要素は登場しないということでもある.

pred show{

NonTransitive[]
}

として推移的ではない例を出してみる.

こいつはA0->A1とA1->A0を結合してA0->A0という関係が元のRにはないので推移的ではない.

こいつはA1->A0とA0->A2を結合してA1->A2が出来るけど元のRには含まれないのでやはり推移的ではない.

これはA1->A0とA0->A2を結合してA1->A2が出来るけど元のRに含まれないのでやはり推移的ではない.

これらは「xはyを知っている」という関係を考えると,この関係は推移的ではないということ.

xがyを知ってて,yがzを知っててもxはzを知っているとは限らないからだ.


前順序(preorder)

pred show{

Preorder[]
}

で見てきます.

前順序(preorder)の定義はこれ.

pred Preorder{

Reflexive[] and Transitive[]
}

反射的で推移的なのが前順序だ.

ってことは全ての要素に自身への対応があって,閉じているのが前順序だ.

前順序は矢印が$\leq$のような等号有りの不等号のようなものとして見做せる関係だ.

以上あるいは以下という順序が決められるものなので当然推移的でなければならない.

年齢による序列は前順序だ.

ただし前順序は全ての要素間に関係があるとは限らない.

序列が決められない場合も認める.

例えば最後から2番目と3番目の例ではA0とA1の間には序列が無い.

集合の要素の包含関係などは前順序と言える.

ジャンケンの強弱関係は推移的ではないので前順序にはならないだろう.

ちなみに後述する半順序との違いは2番目の例や最後の例にあるような異なる要素間の関係として双方向の対応があるか否か.

前順序ではxはy以上でyはx以上というのも含めるが半順序の場合にはそれはもう同じものとして別の要素とは見做さないとも解釈できる.


対称的(symmetric)

pred show{

Symmetric[]
}

で見てきます.

異る要素間に矢印が無いのは良いがあるなら必ず双方向に矢印がないと対称的とはならない.

対称的(symmetric)は$R\in R^{\circ}$ということだが,逆($(-)^{\circ}$)は対合なので,つまり$(R^{\circ})^{\circ} = R$なので,そうすると$R^{\circ}\in R$でもあり,従って$R$と$R^{\circ}$は実質同じとなる.

結局,図の矢印を逆に向けたものが元の図に含まれているのが対称的ということ.

なのでどの矢印も逆向きの関係がある.

この関係は例えば「xがyの配偶者ならばyはxの配偶者だ」ということが言えるようなもの.

友達関係の場合には必ずしもそうとは言えないような友達の定義を訴える人もいよう.

pred NonSymmtetric{

R not in ~R
}

として対称的ではない例も見てみる.

異なる要素間の矢印が一方向にしかないようなところがどこか一箇所でもあれば対称的な射とはならない.


反対称的(anti-symmetric)

pred show{

AntiTransitive[]
}

で見てきます.

反対称的(anti symmetric)は$R\cap R^{\circ}\in iden$なので,Rの矢印を全て逆向きにしたものと元のRにある矢印の共通部分,つまりどちらにも含まれる矢印はidenの中にあるもの,つまり自身の要素への対応に限られる.

異なる要素の間の矢印は一方向だけがあるものだ.

矢印が無いのは構わないが双方向に矢印があるのはダメ.

その場合には$R\cap R^{\circ}$にその異なる要素間の対応(矢印)が含まれてしまうので,そうすると$iden$からはみだしてしまう.

等号なしの大小関係なんかがそうだけど,それだと常に$R\cap R^{\circ}$が空になってしまってちょっとうまい例にはなってないなぁと思うのだが間違いではないということで.


同値(equivalence)

pred show{

Equivalence[]
}

で見てきます.

同値関係そのもの.

同値(equivalence)は

pred Equivalence{

Symmetric[] and Preorder[]
}

となっているが噛み砕くと,$iden\in R$かつ$R\cdot R\in R$かつ$R\in R^{\circ}$だ.

つまり反射的かつ推移的かつ対称的なのが同値.

余談だけどHaskellならEqクラスで,Eqクラスのインスタンスにするには単に(==)を実装すれば良いだけではなく,その(==)の実装が反射律と推移律と対称律を満足するように保証しなくちゃならない.

図でも分るようけど,xとxは同じ(反射的つまり自身への矢印がある)だし,xとyが同じならyとxも同じ(対称的つまり異なる要素間の矢印は双方向にある)だし,xとyが同じでyとzが同じならxとzは同じ(推移的つまり閉じている)というのが見てとれる.


半順序(partial order)

pred show{

Partialorder[]
}

で見てきます.

同値や前順序とかなり似ている.

同値はどの異なる要素間にも矢印が無いかもしくは双方向にある.

半順序の場合にはどの異なる要素間の矢印も無いかもしくはあるなら一方向だ.

前順序の場合には異なる要素間の矢印は無いかもしくは一方向か双方向かいずれでも良い.

半順序は反対称的な前順序.

pred Partialorder{

AntiSymmetric[] and Preorder[]
}

比較のために再掲しよう.

まずは同値.

pred Equivalence{

Symmetric[] and Preorder[]
}

続いて前順序

pred Preorder{

Reflexive[] and Transitive[]
}

半順序は同値の場合に対称的であることを求めるところ,反対称的を求める.

半順序も同値も前順序の子クラスと言える.


余反射的(coreflexive)

pred show{

Coreflexive[]
}

で見てきます.

余反射的(coreflexive)は$R\in iden$なので異なる要素間には矢印はない.

自身へ向かう矢印があるけどすべてにあるとは限らない.

自身に向かう矢印は要素と同一視できるので,その観点からすれば余反射的な射とは要素の部分集合とも取れる.

なお,反射が$iden\in R$なので余反射はこの$\in$の向きが逆になったものだから反射の双対概念で余(co-prefix)が付いてる.

なんかあんまりおもしろくなさそうだけど,AOPでは「あまり知られてないけど重要な概念に余反射があって…」と説明しており論証でもちょこちょこ使ってる模様.


おしまい

今回は射(ここでは関係)の特性についての具体的なイメージを掴むためにalloyでインスタンスを眺めました.

くどいけどこれらの図ひとつひとつが圏論で言うところの一本の射です.

次はsimpleな射とentireな射と言うのを見ていきます.

関数で言えば単射全射みたいなやつかな.(←間違えてる)

圏論ではモノとエピに相当するかと.(←もちろん間違えてる)