前回の記事に檜山さんが反応してくださいまして。いやレスつけにくい記事ですいません。
せっかくなので、檜山さんの記事をまんま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 が直和型です。脳内でそういう風にフィルタかけて読んで下さい。
やってることは見ての通り、１番め・２番め（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
}
}
２項関係に拡張
さてさて、集合（＝単項関係＝アリティ１の関係）について、直和を考えることができました。
次は、２項関係＝アリティ２の関係の直和について。またいちいちこさえます。
fun prod2 (f, g: univ -> univ): Tag -> (univ -> univ) {
Fst -> f + Snd -> g
}prod1 とまったく理屈は同じです。
そして２項関係を考えたからには、他のものとの結合を考えたくなりますね。なりませんか？なるでしょ？
ということで。結合も作ります。（言語要素にないってめんどくさいねー）
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では、２項関係同士の足し算は直接書けて
f+g
なんですなー。
ということで、この２種類の足し算が同じもの、っていう、以下の様なアサーションを書いてみます。反例でないはずです。
sum_equiv: check {
all f, g: univ -> univ | sum2 [f, g] = (f + g)
}
結論
以上、回りくどくなりましたが。
Alloyには表面上プリミティブに存在しない直和ですが、裏側に暗黙的に存在してて、立派に足し算を成立させることができているのです。
ということで、時間があったらこの結果を使って、Alloyで檜山さんの記事を書き直す試みをやってみます。時間があれば。
*1:実は前回も同じようなことを考えて途中でヘタれたのでした。
