bonotakeの日記

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

Alloyで直積を考える

前回の続きです。正確には、前回の続きの後の檜山さんのブログ記事に対する更なる「合いの手」です。

一連の記事を読んでいろいろ考えているうち、実は直和だけでなく直積も問題だということがわかりましたw
ということで、前回とほぼ同じノリで直積も考えてみます。今回も使ったAlloy記述全文はGistに貼りました。
あと、上記檜山さんの記事の「関係圏を観察してみる」以降を適時引用します。Alloyは関係をベースにした言語なので、関係圏とは相性がとてもいいのです。

お膳立て

さっき問題あるとは書いたものの、直積は直和と違い、Alloyにはちゃんと言語機能としてあります。集合A に対して A->A と書きます。
なんで直積なのに関数型みたいな書き方すんの?という方にはこちらを。関係圏では(翻ってAlloyも)集合の直積は冪とか関数(関係だけど)とほぼ同一視できるようです。
ということで、このAlloyの直積を議論の対象として扱います。檜山さんの記事に合わせると、テンソル積と呼ぶべきですかね。

単位元(単位対象)

関係圏Relでは、ホムセット Rel(A, {0, 1}) はAのベキ集合にはなりません。Rel(A, {0}) がAのベキ集合なのです。{0}は単元集合1です。1は、関係圏においては始対象でも終対象でもありません(始対象=終対象=空集合です)。1は、テンソル積(集合の直積でした)の単位対象として特徴付けられます。

だ、そうなので、単元集合を持ってきましょう。
Alloyには特別特定の単元集合があるわけではないので、1からこさえます。と言っても1行で終了ですが。

one sig Unit {}

冒頭のoneで、必ず1個だけ存在する、すなわち単元集合であるという宣言をしております。

で、これがテンソル積の単位対象になってることを確かめてみます。
……といっても、単純じゃないんですよねこれ。要は、 Unit->A ないし A->Unit が Aと同型になっているって言えばいいんですけど。
同型であることの証明ってAlloyで書きづらい……*1

てなわけで、「集合のサイズが等しい」っていう、間接的な形で確認することにします。
ということで、以下のアサーションを。反例出ないと思います。

check {
  all a: set univ {
    #(Unit -> a) = #a
    #(a -> Unit) = #a
  }
}

対角、余対角

対角ですが、こんな感じで。直和の時とほとんど感覚は同じです。

fun diagP (a: univ): univ -> univ {
  a -> a
}

適当な集合Aに対して、A->Aを作って返してやるだけです。
一方余対角ですが、ないらしいので、

論理積∧は、p, q:A→1 に対して、δA;(p×q);ρ と定義する。ρ:1×1→1 は、テンソル積の単位法則に伴う自然同型。

にあるρ:1×1→1 (ここまでの書き方に沿えば、ρ:(Unit->Unit)->Unit)をこさえましょう。こんな感じです。

fun ro (r: Unit -> Unit): Unit {
  Unit.r
}

rの頭からUnitと結合して、r: Unit->Unitの後ろ側の成分(第二成分)だけを取り出して返します。
え?第一成分は要らないの?これでいいの?? とお思いになるかもしれませんが……一般的にはダメかもしれません。しかしAlloyの矢印型直積を使う分には、これで構いません。この理由は後で述べます。
で、せっかくなので、上記論理積 δA;(p×q);ρ を作ってしまいましょう。 まずは δA と (p×q) を結合するために、次のような関数をこさえます。

fun joinL (a: univ->univ, r: (univ->Unit)->(univ->Unit)): Unit->Unit {
  (a.univ).(r.univ.univ) -> (univ.a).(univ.(univ.r))
}

aの第一成分とrの第一成分、第二成分と第二成分を結合して、改めて -> でつなぎなおします。これも、直和のときに考えた結合と、基本的な理屈は同じです。

以上の diagP(δA)とjoinL(結合子 ; )、ro(ρ)をつないで、さっきの論理積の定義を書き下します。

fun prodL (f,g: univ -> Unit): univ -> Unit {
  {x: univ, u: Unit | u = x.diagP.joinL [f -> g].ro }
}


こうして、論理積 f ∧ g が定義できたんですけども。
これって結局、やっぱり、Alloyでいうところの

f & g

と同じなんですよね。実際、以下のアサーションは反例出ないです。

equiv_product: check {
  all f, g: univ -> Unit | prodL[f, g] = f & g
}

ということで、直和の時とオチもほぼ同じでした。ちゃんちゃん。

ちなみに、以前紹介したドメイン付きクリーネ代数のAlloyモデルですが、命題をPropのべき集合(set Prop)で与え、論理積はその間の集合積 & で書いてました。この辺とややつながった感じ?

直積にもいろいろある

で、上記 ro の定義がなんであんないい加減でいいのか、というお話ですが。
実は、ひとくちに「直積」と言っても、ビミョーな差でいくつか種類があるのです。それで「Alloyの矢印型直積を使う分にはこれで構わない」なんてビミョーな表現をしたのです。


ro の引数 r: Unit -> Unit (=Unit×Unit)ですが、具体的に何種類の値があるかわかります?
Unitが単元集合だったので、Unit型の引数にはたかだか1要素しか入りません。なのでUnit×Unitなら、第一成分、第二成分それぞれに「ある」(Unitそのもの)か「ない」(空集合 none)かの2択しかなく、よって r は 4種類。
……と見せかけて、実はAlloyの場合、2種類しかありません。Alloyの直積はstrictな直積(スマッシュ直積とかいいます)になっていて、片方の成分が空集合なら、ただちに全体も空集合になります*2。なので、第一成分、第二成分とも「ある」か、両方ともなかったことになるかの2択なのです。
一方、一般的な集合の直積、集合圏の直積はstrictではなく、なので片方が空集合というだけで全体が空集合と完全にイコールにはなりません(同型にはなるけど)。ということで、ビミョーに違うんですね。
なので roは、本当なら「第一成分と第二成分がともに空でない場合に単元集合を返す、そうでなければ空集合を返す」と書くべきなんでしょうが。現実的には、どっちも空でないかどっちも空か、しか選択肢がないので、片方だけ参照する、という上の定義で成り立ってるわけです。

Alloyプリミティブの直積 -> じゃなくて、新たに一般的な直積を起こせばよかったのかもしれませんが、面倒くさかったのでした。はい。

*1:天下りに同型射を与えればいいんですけどね。

*2:スマッシュ直積云々はこちらでもちらっと書いてますが、って8年半も前の記事だよ。わーお。

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