Alloyで直和を考える - bonotakeの日記

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

クリーニ代数と圏論 - 檜山正幸のキマイラ飼育記

せっかくなので、檜山さんの記事をまんま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:実は前回も同じようなことを考えて途中でヘタれたのでした。