bonotakeの日記

ソフトウェア工学系研究者 → AIエンジニア → スクラムマスター・アジャイルコーチ

Alloyで直和を考える

前回の記事に檜山さんが反応してくださいまして。いやレスつけにくい記事ですいません。

せっかくなので、檜山さんの記事をまんまAlloyに翻訳してみよう…と思ったのですが*1、実は大きな問題があって。

Alloyには、直和を直接扱う言語要素がないんですなー。

ということで前振りとして、Alloyで直和を書き下してみて、どうなるかってのを観察してみます。

今回使うAlloyの記述全文はGistに貼ったので、よろしければそちらを参照のこと。

えーまず

いきなりですが、直和をこさえます。どーん。

enum Tag { Fst, Snd }

fun prod1(a, b: univ): Tag -> univ {
  Fst -> a + Snd -> b
}

prod1が、適当な集合a, bを受け取って(univは何でもアリな型です。java.lang.Objectみたいな)、aとbの直和を返す関数。返り値の型 Tag -> univ が直和型です。脳内でそういう風にフィルタかけて読んで下さい。
やってることは見ての通り、1番め・2番め(Fst, Snd)ってタグを付けた上で集合和を取るんですね。
prod って書いてるのは、上記の檜山さんの記事にある「(圏論的)直積=(圏論的)直和」に倣ってるので、ここでは良いネーミングじゃないかもですが。

試しに

run prod1

とか打ってevaluate ... してみても、ビジュアル的にはあんまり面白くないものが出ます。Evaluatorボタンを押して、prod1に適当な引数渡して評価してみてください。

対角、余対角

さて、任意の要素を直和に持っていく対角Δは次のように書けます。

fun diag (a: univ): Tag -> univ {
  Fst -> a + Snd -> a
}

diagがΔに相当する関数です。Fstタグ、Sndタグに同じ要素を入れた直和を返します。

一方、直和から要素に潰す余対角∇は

fun codiag (a: Tag -> univ): univ {
  { b: univ | b in Fst.a or b in Snd.a }
}

とか書けます。直和のFstタグ側かSndタグ側か、どちらかにある要素の集合、です。
…ですがこれ、もっと簡単にかけて、

fun codiag (a: Tag -> univ): univ {
  Tag.a
}

です。ついてるタグを忘れる操作。


そして、対角と余対角を合成すると、idと同じになります。
これは以下のアサーションで反例が出ないことからわかっていただけるかと。

cmp_id: check {
  all x: univ | x.diag.codiag = x
}

単位元

さてここで、直和操作の単位元について考えてみます。これは、空集合Alloyでいう none)でございます。檜山さんの記事にあった、零対象がこれに当たります。
noneとの直和取ったものは元の要素と同型です。
これは、noneとの直和取って、タグ忘れたら元に戻る、という意味の以下のアサーションで反例が出ないことから確かめられます。

zero_is_unit1: check {
  all x: univ {
    prod1 [x, none].codiag = x
    prod1 [none, x].codiag = x
  }
}

2項関係に拡張

さてさて、集合(=単項関係=アリティ1の関係)について、直和を考えることができました。
次は、2項関係=アリティ2の関係の直和について。またいちいちこさえます。

fun prod2 (f, g: univ -> univ): Tag -> (univ -> univ) {
  Fst -> f + Snd -> g
}

prod1 とまったく理屈は同じです。

そして2項関係を考えたからには、他のものとの結合を考えたくなりますね。なりませんか?なるでしょ?
ということで。結合も作ります。(言語要素にないってめんどくさいねー)

fun join2 (x: Tag -> univ, r: Tag -> (univ -> univ)): Tag -> univ {
  Fst -> (Fst.x.(Fst.r)) + Snd -> (Snd.x.(Snd.r))
}

わかりますでしょうか。Fstタグ付きはFstタグ付き同士、Sndタグ付きはSndタグ付き同士で結合して、改めてタグを付け直しております。
直感的には x.r って操作をやりたい訳なんですが、直接は上手くいかないので、この関数で結合のドットを代用しようという腹です。

で、こうしてやると、元の檜山さんの記事にあった足し算の定義

Δ;(f×g);∇

ってのが書けるようになります。こんな↓感じ。

fun sum2 (f, g: univ -> univ): univ -> univ {
  { x, y: univ | y in x.diag.join2 [ prod2 [f, g] ].codiag }
}

diagがΔ、prod2[f,g] が f×g、codiagが∇。
適当なxに対して y ∈ x;Δ;(f×g);∇ となるようなyを集めて、ペア (x, y) の集合を作っているわけです。2項関係はペアの集合でできています。よってこれは、間に Δ;(f×g);∇ が成り立つような2項関係を作っているわけです。

これも run sum2 とかやって、Evaluatorで遊んでみてくださいな。


しかし、ですね。
Alloyでは、2項関係同士の足し算は直接書けて

f+g

なんですなー。

ということで、この2種類の足し算が同じもの、っていう、以下の様なアサーションを書いてみます。反例でないはずです。

sum_equiv: check {
  all f, g: univ -> univ | sum2 [f, g] = (f + g)
}

結論

以上、回りくどくなりましたが。
Alloyには表面上プリミティブに存在しない直和ですが、裏側に暗黙的に存在してて、立派に足し算を成立させることができているのです。

ということで、時間があったらこの結果を使って、Alloyで檜山さんの記事を書き直す試みをやってみます。時間があれば。

*1:実は前回も同じようなことを考えて途中でヘタれたのでした。

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。