bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

Alloyで圏論

Alloyなる仕様記述言語 (本家サイト)で圏の定義を書いてみました。なぜAlloyかは、一応目的はあるので続きがあれば書きますが、特に深い意味はないです。仕様記述言語なら何でも良かったという話も。
でもここに書いてわかる人も少ないと思うし、現状、ほとんど自分向けのメモです。


で、以下が間違ってるかもしれないけどそれ。

sig Object {}
sig Category {
	objs: set Object, // 対象の集合
	hom: objs -> objs // 射の集合(hom集合)
}
{
	objs <: iden in hom // 恒等射の存在
	hom.hom in hom // 追加:composition について閉じている
}

当然色つかないよな、うん。
本当は、ちょーっとidの定義がよろしくないのですが、とりあえずほっときます。組み込みでidenなるものがあったんで、そっち使うよう修正しました。
iden てのは、恒等写像全体の集合です。"<:"などという紛らわしい記号は、ドメインを限定するためのもの。"objs <: iden" で、objs をドメインとしている恒等写像全体の集合が得られます。

結合性は、Alloyがベースにしてる relational logic*1 の特質から、明示しなくても言えてしまうと思われます。実際、以下の表明が通ります。

assert associative {
	all f,g,h : Category.hom {
		f.(g.h) = (f.g).h
	}
}

以下蛇足ですが、これで*2

check associative

とか書くと

Executing "Check associative"
   Solver=sat4j Bitwidth=4 MaxSeq=4 Symmetry=20
   613 vars. 69 primary vars. 1191 clauses. 125ms.
   No counterexample found. Assertion may be valid. 125ms.

とかなって反例なし。

*1:RDBMSのそれとは似て非なるものなので注意。

*2:Alloy の "." は、圏論の";"と同じで、左から右へのcomposition(みたいなもの)です。f.g ≒ f;g = g o f。Alloyでは dot join とか言ってます。

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