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.
とかなって反例なし。