| title | tags | author | slide |
|---|---|---|---|
Coq で圏論：背景と普遍性について |
Coq-8.5 Coq |
mathink |
false |
- そもそもどんな風に Coq で圏論やってるのかという話
- 存在性と唯一性で構成される普遍性を「函数とその性質」という形に変換して記述した
- 証明を割愛するという暴挙
- 参照しているソースコード
- それをライブラリ化したもの
暇つぶしに、 Coq 上で Setoid ベースの構成的な圏論をやっている。 どういうことかというと、
- 普通の圏論における局所小(locally small)な圏を基準に、
- 普通の圏論における「集合」を Setoid で置き換えて、
- なるべく
existsを使わないで構成的に圏論を展開
という感じ。
「性質 P を持つ Ｘ が存在する」をそのまま exists X, P(X) みたいに書くのではなくて、存在するなら実際に作ってみせよ、というスタンスです。
命題の形にしてしまうと、存在するという事実から実体を取り出せず、圏論的な理論展開をほぼ全部命題ベースで行なわなければならなくなります。 そうしてしまうと、 Coq 上のデータが実はある種の圏論的な構成として得られるのでしたーという時に、それまで展開していた(Coq 上での)圏論の資産を直接利用できません。
要するに、圏とか函手とか直積とか直和とか、そういったものをデータ型として定義して、「圏論」としてそのデータ型を持つもの同士の関係を記述することで、 Coq 上のプログラミングにも応用可能な理論を展開できるといいなぁということです。
圏論において重要なのは射、そして射の関係を記した図式です。 図式は即ち射の間の等価性ですから、射の等価性をどう記述するかが重要になります。
その等価性として Coq の eq をそのまま使うのはあまりよろしくありません。
なぜかといえば、 eq には既に「Coq 上の項として等しい」という意味が与えられているので、射の種類によっては本来想定している等価性の意味とそぐわないことがあるからです。
たとえば、函数を射とする圏を考えるとき、函数の等価性として外延的等価性(つまり forall x, f x = g x)を想定していた場合、 Coq では Axiom なしには整合性を取ることができません。
(実際、射の等価性として無条件に eq を採用してしまうと State モナドが (圏論的には) Axiom なしに定義できなくなります)
そこで、圏 C の対象 X, Y について Hom(X,Y) を Setoid にすることで、等価性をより柔軟に扱えるようにしているのが Setoid ベースでのアプローチです。
Coq 上で展開するにあたって都合のよい条件だったからです。 函数型プログラミングとの相性的にも、これでよいのでは、という気がしています。
あと、 small な圏を Coq で定義しようとすると大変な目にあいます(気になる方はやってみてください)。
なんとなくですが、集合を利用した圏論における locally smallness と Setoid ベースの圏論における locally smallness は微妙に意味が違っているような気がしています。
圏論的な構成物 X は、基本的に
- X の性質を一つに纏めた型クラス
Class IsX - X の構成物を一つに纏めた構造
Structure Xの二つでもって定義していきます。
一纏めにしないのは、「X が Hoge となる」というステートメントを素直に IsHoge X と記述するためです。
たとえば「函手 F が極限を保存する」という命題を書こうとすると、どちらも出てきます(それぞれの具体的定義は今は置いておきます)。
Class PreserveLimit
(J C C': Category)
(F: C --> C')
(D: J --> C)
(lim: Limit D)
(univ: forall c : Cone (F \o D),
C' c (compose_cone F lim)) :=
preserve_limit: IsLimit univ.あと、データ型を記述するために Class を使いたくない、という個人的理由もあります。
仕様と構成を Class と Structure に分けたので、通常ならば、ある圏論的対象 Hoge を実際に構成する時、
xやyがIsHogeを満たすことを示す- その証明から
Hoge型のデータを構成する という二段階のステップを踏むことになります。
ですが、一々 2 ステップ踏むのが面倒なので、 Notation と Program コマンドを組み合わせることで、データの定義時に必要な分のゴールを生成し証明モードに入れるようにしています。
基本的に [Hoge by foo] という形式で、 foo を利用して Hoge 型のデータが定義できるようになっています。
たとえば、右 Kan 拡張から極限を構成する際は以下のようなコマンドになります。
Program Definition limit_from_ran
(C D: Category)
(F: C --> D)
(ran: Ran F (ToOne C))
: Limit F :=
[Limit [Cone by (ranN ran) from (ranF ran tt)]
by `(ranU ran (S:=[* in One |-> (c: Cone F) in D]) [i :=> c i] tt) ].このコマンドを実行すると証明モードに入り [Cone by (ranN ran) from (ranF ran tt)] が実際に F の極限であることを求められるわけです(更に言えば頂点 ranF ran tt とが射の族 ranN ran を伴って錐をなすことの証明も求められます。入れ子にして使うこともできるということです)。
Setoid の定義から圏の定義までを追います。
Require Export Coq.Program.Basics Coq.Program.Tactics Coq.Setoids.Setoid Coq.Classes.Morphisms.前半二つは Program コマンドを多用するにあたって必要なものです。
後半二つは Setoid 上の等価性について rewrite を使うために必要です。
Coq.Setoids.Setoid に Setoid は定義されてないので、上書きを気にせず Setoid 型を定義していきましょう。
さっそくですが、冗長なため IsSetoid はありません。
Structure Setoid: Type :=
{
setoid_carrier:> Type;
setoid_equal: setoid_carrier -> setoid_carrier -> Prop;
setoid_prf:> Equivalence setoid_equal
}.
Existing Instance setoid_prf.
Notation "[ 'Setoid' 'by' P 'on' A ]" := (@Build_Setoid A P _).
Notation "[ 'Setoid' 'by' P ]" := [Setoid by P on _].
Notation "(== 'in' A )" := (setoid_equal A).
Notation "x == y 'in' A" := (setoid_equal A x y) (at level 70, y at next level, no associativity).
Notation "(==)" := (== in _).
Notation "x == y" := (x == y in _) (at level 70, no associativity).Notation "[ 'Setoid' 'by' P 'on' A ]" := (@Build_Setoid A P _).の部分(と似たようなやつ)が Program コマンドと組み合わせて使うための Notation です。
次のように使います。
Program Definition eq_setoid (X: Type) :=
[Setoid by @eq X].Program Definition function (X Y: Type): Setoid :=
[Setoid by `(forall x, f x = g x) on X -> Y].function の定義では Generalizable All Variables オプションを利用しています(気になる方は これ とか読んでみてください)。
locally small 的に圏を定義していきます。
まずは仕様を表わす型クラス IsCategory です。
Class IsCategory
(obj: Type)
(hom: obj -> obj -> Setoid)
(comp: forall {X Y Z: obj}, hom X Y -> hom Y Z -> hom X Z)
(id: forall (X: obj), hom X X) :=
{
cat_comp_proper:>
forall (X Y Z: obj),
Proper ((==) ==> (==) ==> (==)) (@comp X Y Z);
cat_comp_assoc:
forall X Y Z W (f: hom X Y)(g: hom Y Z)(h: hom Z W),
comp f (comp g h) == comp (comp f g) h;
cat_comp_id_dom:
forall X Y (f: hom X Y),
comp (id X) f == f;
cat_comp_id_cod:
forall X Y (f: hom X Y),
comp f (id Y) == f
}.
Hint Resolve cat_comp_assoc cat_comp_id_dom cat_comp_id_cod.圏を構成するのは
- 対象の型
obj - 対象から射の Setoid への割り当て
hom - 射の合成
comp - 恒等射
idなので、これらの四つの要素に関する述語として、記述しています。
各フィールドは圏の公理を表わしていますが、注意すべきは cat_comp_proper です。
これは comp が射の等価性を保存していることを意味します。
これにより、たとえば仮定に Heq: f == g があるときにゴール f \o k == g \o k に対し、 rewrite Heq が出来るようになります。
今後も、射の上の変換が現われた際は Proper を利用することが多いです。
Proper についての詳細は A Gentle Introduction to Type Classes and Relations in Coq を読むとよいと思います。
次に、圏の型 Category を定義します。
Structure Category :=
{
cat_obj:> Type;
cat_hom:> cat_obj -> cat_obj -> Setoid;
cat_comp:
forall (X Y Z: cat_obj),
cat_hom X Y -> cat_hom Y Z -> cat_hom X Z;
cat_id: forall X: cat_obj, cat_hom X X;
cat_prf:> IsCategory cat_comp cat_id
}.
Existing Instance cat_prf.
Notation "[ 'Category' 'by' hom 'with' comp , id ]" :=
(@Build_Category _ hom comp id _).
Notation "[ 'Category' 'by' hom 'with' 'comp' := comp 'with' 'id' := id ]" :=
[Category by hom with comp , id].
Notation "g \o{ C } f" := (@cat_comp C _ _ _ f g) (at level 60, right associativity).
Notation "g \o f" := (g \o{_} f) (at level 60, right associativity) .
Notation "Id_{ C } X" := (@cat_id C X) (at level 20, no associativity).
Notation "'Id' X" := (Id_{_} X) (at level 30, right associativity).基本的に、仕様 IsHoge を記述する際に必要だった構成要素をフィールドとして持ち、最後のフィールドとして、それらが仕様を満たすことを意味するフィールド hoge_prf を用意します。
このやり方は基本的に全ての構成について共通です。
ここで、 Program 用の Notation の他、射の合成や恒等射についても記法を幾つか定義しました。
また coercion を利用することで、 Hom(X,Y) を C X Y と書けるようにしてあります(文献によっては hom を C(X,Y) と書くのに倣っています)。
何も具体例がないのは寂しいので Type の圏と Setoid の圏を作ります。
基本的に Program Definition のあとは証明が必要ですが、割愛します。
Type の圏では、函数が射です。ここでは射の等価性として外延的等価性を採用したので、 hom setoid は function です。
Program Definition Types :=
[Category by function
with (fun X Y Z f g x => g (f x)),
(fun X x => x)].Setoid の圏を定義するにはまず Setoid 間の射を定義する必要があります。
X Y: Setoid に対して、 X と Y の間の変換を表わす Map X Y という型を定義します。
Class IsMap {X Y: Setoid}(f: X -> Y) :=
{
map_proper:> Proper ((==) ==> (==)) f
}.
Structure Map (X Y: Setoid): Type :=
{
map_fun:> X -> Y;
map_prf:> IsMap map_fun
}.
Existing Instance map_prf.
Notation "[ 'Map' 'by' f ]" := (@Build_Map _ _ f _).
Notation "[ x 'in' X :-> m ]" := [Map by fun (x: X) => m].
Notation "[ x :-> m ]" := ([ x in _ :-> m]).ここでも Proper が出てきました Setoid の等価性を保存することを表わしています(well-definedness ですね)。
Setoid の carrier type 間の函数のうち、 well-defined なものを Setoid の間の変換とする、ということです。
そして、圏を定義するには、 hom setoid 、合成、恒等射が要るので、それぞれ作ります
Program Definition Map_compose (X Y Z: Setoid)(f: Map X Y)(g: Map Y Z): Map X Z :=
[ x :-> g (f x)].Program Definition Map_id (X: Setoid): Map X X :=
[ x :-> x ].Program Definition Map_setoid (X Y: Setoid): Setoid :=
[Setoid by `(forall x, f x == g x) on Map X Y].必要な道具が準備出来たので Setoid の圏 Setoids を構成します。
Program Definition Setoids :=
[Category by Map_setoid with Map_compose, Map_id].あっさりしていますが、そんなもんです(証明は必要ですが)。
ちなみに、通常の圏論で集合の圏 Sets が為す役割を、 Setoid ベースの圏論ではこの Setoids が担うことになります(が、本記事では触れません)。
これが本題です。
普遍性というのはたいていの場合「A が Hoge であるとは、性質 P を満たす X に対して、性質 Q を満たす Y が唯一存在すること」と記述されるのですが、それを「A と "性質 P を満たす X に対して Y を与える" univ の組 (A, univ) が Hoge であるとは、 univ が性質 Q を満たし、かつ同一の性質を持つ (A', univ') について univ = univ' である」と読み替え、 Coq 上で定義していきます。
これだけだと何が何だかだと思うので、以下、具体例を見ていきましょう。
圏
まず、この文言をそのまま命題として書き下してみます。
Definition IsInitial (C: Category)(i: C) :=
forall (X: C), exists f: C i X, True.こんなところでしょうか。 文言の、 Coq 上の命題への翻訳としては問題ありません。
ですが、構成的に圏論を展開していきたいとなると、 exists は厄介ですね。
始対象 i が与えられたとき(つまり IsInitial i の証明があるとき)、始対象であるという事実(証明項)から、具体的なデータを得ることができないからです。
「任意の対象 X への射が唯一つ存在」すると言っているのですから、時によってはその射を使って別の何かを作りたいときも出てくるわけですが、「始対象であること」をこのように記述すると、そうして作られた何かもまた証明項の中に押し込めておくしかないですね。
そうなってしまうのは、存在性を命題の記述に使っているからなので、そこを上手く取り除きたいです。
ということで、始対象の定義を次のように読み替えます。
「圏
少々天下り感はありますが、こうすることで、「始対象である」という仕様の中に存在性が含まれなくなりました。 「そもそも存在すると言っているのだから与えられるだろう」という構成的なスタンスに則った言い換えです。
さて、この文言を Coq 上に書き下すと次のようになります。
Class IsInitial (C: Category)
(obj: C)
(univ: forall X: C, C obj X) :=
{
initial_uniqueness:
forall (X: C)(u: C obj X),
u == univ X
}.そして「C の始対象」を表わすデータ型が次のように定義されます。
Structure Initial (C: Category) :=
{
initial_obj:> C;
initial_univ: forall X: C, C initial_obj X;
initial_prf:> IsInitial initial_univ
}.
Existing Instance initial_prf.
Notation "[ 'Initial' i 'by' univ ]" := (@Build_Initial _ i univ _).
Notation "[ 'Initial' 'by' univ ]" := [Initial _ by univ].Initial 型を定義しておくことで、 i: Initial C と書けばデータとして C の対象 i と u: forall X, C i X を得ることが出来るようになります。
同様の流れで、終対象を表わす仕様 IsTerminal と型 Terminal も定義することができます。
Class IsTerminal (C: Category)
(obj: C)
(univ: forall X: C, C X obj) :=
{
terminal_uniqueness:
forall (X: C)(f: C X obj),
f == univ X
}.
Structure Terminal (C: Category) :=
{
terminal_obj:> C;
terminal_univ: forall X: C, C X terminal_obj;
terminal_prf:> IsTerminal terminal_univ
}.
Existing Instance terminal_prf.
Notation "[ 'Terminal' t 'by' univ ]" := (@Build_Terminal _ t univ _).
Notation "[ 'Terminal' 'by' univ ]" := [Terminal _ by univ].始対象と終対象は普遍的構成としては極めて単純ですが、 Coq 上で構成的に圏論をやるとき、「普遍的な hoge」の扱いがどうなるのかの雰囲気を感じ取ることはできるのではないでしょうか。
では、せっかくなので Types と Setoids における具体例を載せておきます。
Inductive empty := .
Program Definition initial_of_Types: Initial Types :=
[Initial empty by (fun (X: Type)(e: empty) => match e with end)].
Program Definition empty_setoid: Setoid :=
[Setoid by (fun e e' => match e, e' with end) on empty].
Program Definition initial_of_Setoids: Initial Setoids :=
[Initial empty_setoid
by (fun (X: Setoid) => [e in empty :-> match e with end])].Inductive unit := tt.
Program Definition terminal_of_Types: Terminal Types :=
[Terminal unit by (fun (X: Type)(_: X) => tt)].
Program Definition unit_setoid: Setoid :=
[Setoid by (fun x y => True) on unit].
Program Definition terminal_of_Setoids: Terminal Setoids :=
[Terminal unit_setoid by (fun (X: Setoid) => [_ in X :-> tt])].まず、直積の定義は以下の通りです。
「圏
これを構成的に言い換えて Coq 上に書き下したものは以下のようになります。
Class IsProduct (C: Category)(X Y: C)
(P: C)(pi1: C P X)(pi2: C P Y)
(univ: forall (Z: C), C Z X -> C Z Y -> C Z P) :=
{
product_universality_1:
forall (Z: C)(p1: C Z X)(p2: C Z Y),
(p1 == pi1 \o univ Z p1 p2);
product_universality_2:
forall (Z: C)(p1: C Z X)(p2: C Z Y),
(p2 == pi2 \o univ Z p1 p2);
product_uniqueness:
forall (Z: C)(p1: C Z X)(p2: C Z Y)(u: C Z P),
(p1 == pi1 \o u) ->
(p2 == pi2 \o u) ->
u == univ Z p1 p2
}.始対象や終対象の時と違い、 universality という形でフィールドに記述しました。
_1 と _2 があるのは、 /\ で繋ぎたくなかっただけなので、たとえば
product_universality:
forall (Z: C)(p1: C Z X)(p2: C Z Y),
(p1 == pi1 \o univ Z p1 p2)/\(p2 == pi2 \o univ Z p1 p2);と一纏めにしても問題はありません。
そして圏 C における X と Y の直積を表わす型 Product C X Y は次のように定義できます。
Structure Product (C: Category)(X Y: C) :=
{
product_obj:> C;
product_proj1: C product_obj X;
product_proj2: C product_obj Y;
product_univ: forall (Z: C), C Z X -> C Z Y -> C Z product_obj;
product_prf:> IsProduct product_proj1 product_proj2 (@product_univ)
}.
Existing Instance product_prf.
Notation "[ 'Product' P 'by' univ 'with' pi1 , pi2 ]" :=
(@Build_Product _ _ _ P pi1 pi2 univ _).
Notation "[ 'Product' 'by' univ 'with' pi1 , pi2 ]" :=
[Product _ by univ with pi1, pi2].
Notation "[ f , g 'to' P ]" := (product_univ P f g).
Notation "pi1_{ P }" := (product_proj1 P) (at level 0, no associativity, format "pi1_{ P }").
Notation "pi2_{ P }" := (product_proj2 P) (at level 0, no associativity, format "pi2_{ P }").双対なんで、直和もまとめてやっちゃいましょう。
「圏
Class IsCoproduct (C: Category)(X Y: C)
(CP: C)(in1: C X CP)(in2: C Y CP)
(univ: forall (Z: C), C X Z -> C Y Z -> C CP Z) :=
{
coproduct_universality_1:
forall (Z: C)(i1: C X Z)(i2: C Y Z),
(i1 == univ Z i1 i2 \o in1);
coproduct_universality_2:
forall (Z: C)(i1: C X Z)(i2: C Y Z),
(i2 == univ Z i1 i2 \o in2);
coproduct_uniqueness:
forall (Z: C)(i1: C X Z)(i2: C Y Z)(u: C CP Z),
(i1 == u \o in1) ->
(i2 == u \o in2) ->
u == univ Z i1 i2
}.
Structure Coproduct (C: Category)(X Y: C) :=
{
coproduct_obj:> C;
coproduct_inj1: C X coproduct_obj;
coproduct_inj2: C Y coproduct_obj;
coproduct_univ: forall (Z: C), C X Z -> C Y Z -> C coproduct_obj Z;
coproduct_prf:> IsCoproduct coproduct_inj1 coproduct_inj2 (@coproduct_univ)
}.
Existing Instance coproduct_prf.
Notation "[ 'Coproduct' P 'by' univ 'with' in1 , in2 ]" :=
(@Build_Coproduct _ _ _ P in1 in2 univ _).
Notation "[ 'Coproduct' 'by' univ 'with' in1 , in2 ]" :=
[Coproduct _ by univ with in1, in2].
Notation "[ f , g 'from' P ]" := (coproduct_univ P f g).
Notation "in1_{ P }" := (coproduct_inj1 P) (at level 0, no associativity, format "in1_{ P }").
Notation "in2_{ P }" := (coproduct_inj2 P) (at level 0, no associativity, format "in2_{ P }").そして、今回も Types と Setoids における具体例を構成していきます。
まずは直積です。
Record product (A B: Type): Type :=
pair_of { fst: A; snd: B }.
Notation "( x , y )" := (pair_of x y) (format "( x , y )").
Notation "p .1" := (fst p) (at level 5, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 5, left associativity, format "p .2").
Program Definition product_of_types (X Y: Type)
: Product Types X Y :=
[Product (product X Y) by (fun P f g x => (f x, g x))
with @fst X Y, @snd X Y].
Program Definition product_setoid (X Y: Setoid): Setoid :=
[Setoid by `((p.1 == q.1) /\ (p.2 == q.2)) on product X Y].
Program Definition product_of_Setoids (X Y: Setoid)
: Product Setoids X Y :=
[Product (product_setoid X Y)
by (fun P f g => [x :-> (f x, g x)])
with [Map by @fst X Y], [Map by @snd X Y]].次に直和です。
Inductive coproduct (A B: Type): Type :=
| inj1: A -> coproduct A B
| inj2: B -> coproduct A B.
Program Definition coproduct_of_Types (X Y: Type)
: Coproduct Types X Y :=
[Coproduct (coproduct X Y)
by (fun P f g xy => match xy with
| inj1 _ x => f x
| inj2 _ y => g y
end)
with @inj1 X Y, @inj2 X Y].
Program Definition coproduct_setoid (X Y: Setoid) :=
[Setoid by (fun a b => match a, b with
| inj1 _ x, inj1 _ x' => x == x' in X
| inj2 _ y, inj2 _ y' => y == y' in Y
| _, _ => False
end)].
Program Definition coproduct_of_Setoids (X Y: Setoid)
: Coproduct Setoids X Y :=
[Coproduct (coproduct_setoid X Y)
by (fun P f g => [xy :-> match xy with
| inj1 _ x => f x
| inj2 _ y => g y
end])
with [Map by @inj1 X Y],
[Map by @inj2 X Y]].駆け足ですが、 Coq 上で圏論を展開するにあたって普遍的構成をどのように記述しているのか、それを簡単な例でもって示してみました。 実のところ、参照しているコード(これ)には上記の例の他、羃、(コ)イコライザ、(余)極限、Kan 拡張といった普遍的構成も含まれています。 興味のある方は、実際に CoqIDE とか ProofGeneral 上でいじってみるとよいかもしれません。
近々 Cat_on_Coq を大規模破壊的更新するので、その後に軽く紹介記事でも書くと思います。 というか、圏論の主役であるところの函手と自然変換が影も形もなかったので、それを扱いたいですね。