Alloyで直積を考える

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

• Alloyで直和を考える - たけをの日記＠天竺から帰ってきたよ
• 個体と世界の関係：圏から論理半環を絞り出す - 檜山正幸のキマイラ飼育記

一連の記事を読んでいろいろ考えているうち、実は直和だけでなく直積も問題だということがわかりましたｗ
ということで、前回とほぼ同じノリで直積も考えてみます。今回も使った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年半も前の記事だよ。わーお。