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 とか言ってます。