| title | tags | author | slide |
|---|---|---|---|
Coq で圏論：自然変換とデータ型 |
Coq Coq-8.5 |
mathink |
false |
- Coq 上で自然変換を定義
- 米田の補題を示してみた(証明そのものは省略)
listとかtreeと自然変換の関連を見た- 記事の元ネタのライブラリ(Cat_on_Coq)はここ
以下の記事を読んでおくとわかりやすいかもしれません。
証明は省略していますが、ほぼ全て rewrite です。
二つの函手
を満たすもののことです。
この条件を仕様として書き下した型クラス IsNatrans は次のようになります。
自然変換は Natural transformation ですが、長いので、私は Natrans と表記しています。
Class IsNatrans
(C D: Category)
(F G: C --> D)
(natrans: forall (X: C), D (F X) (G X)) :=
{
natrans_naturality:
forall (X Y: C)(f: C X Y),
natrans Y \o fmap F f == fmap G f \o natrans X
}.
そして F から G への自然変換の型 Natrans F G は以下のようになります。
Structure Natrans {C D: Category}(F G: C --> D): Type :=
{
natrans:> forall X: C, D (F X) (G X);
natrans_prf:> IsNatrans natrans
}.
Existing Instance natrans_prf.
Notation "F ==> G" := (Natrans F G).
Notation "[ X 'in' T :=> f 'from' F 'to' G ]" := (@Build_Natrans _ _ F G (fun X: T => f) _).
Notation "[ X :=> f 'from' F 'to' G ]" := [X in _ :=> f from F to G].
Notation "[ X 'in' T :=> f ]" := [X in T :=> f from _ to _].
Notation "[ X :=> f ]" := ([ X in _ :=> f]).自然変換
射としての自然変換の等価性は
で定義します。この定義でもって Natrans F G 上の Setoid を定めます。
この Setoid が Fun C D の hom setoid になります。
Program Definition Natrans_setoid (C D: Category)(F G: C --> D): Setoid :=
[Setoid by (fun (S T: F ==> G) => forall X, S X == T X)].
Canonical Structure Natrans_setoid.そして、
Program Definition Natrans_compose (C D: Category)(F G H: C --> D)(S: F ==> G)(T: G ==> H): F ==> H :=
[X :=> T X \o S X].
Program Definition Natrans_id (C D: Category)(F: C --> D): Natrans F F :=
[X :=> Id (F X)].ということで、 C から D への函手の圏 Fun C D を次のように定義します。
Program Definition Fun (C D: Category): Category :=
[Category by (@Natrans_setoid C D)
with (@Natrans_compose C D), (@Natrans_id C D)].
Canonical Structure Fun.
Notation "D ^ C" := (Fun C D).有名なやつですね。圏、函手、自然変換、集合(Setoid)という、圏論の基本登場人物がまとめて登場する定理なので、やっておくとこれまでの議論の確認になっていいのではないかな、と思い、やってみました。
米田の補題は、通常の圏論であれば、集合の圏
が成り立つ、というものです。
ここで、
Coq 上での圏論では「集合」を Setoid に読み替えて議論をしていましたので、この言明を Coq 上に書くと、次のようになります。
Theorem yoneda_lemma:
forall (C: Category)(X: C)(F: C --> Setoids),
equiv ((Setoids^C) Hom(X,-) F) (F X).ここで、 equiv は以下のようにして定義されてる関係です。
Definition injective (X Y: Setoid)(f: Map X Y) :=
forall x y, f x == f y -> x == y.
Definition surjective (X Y: Setoid)(f: Map X Y) :=
forall (y: Y), exists x: X, f x == y.
Definition bijective (X Y: Setoid)(f: Map X Y) :=
injective f /\ surjective f.
Definition equiv (X Y: Setoid) :=
exists f: Map X Y, bijective f.米田の補題そのものの証明はググれば出てきますしそもそもあまり難しくないので割愛します。 一応、 Coq 上での証明だけ記しておきます(定義など、記事に載せている順番が実際のコードとは異なるので注意してください)。
Theorem yoneda_lemma:
forall (C: Category)(X: C)(F: C --> Setoids),
equiv ((Setoids^C) Hom(X,-) F) (F X).
Proof.
intros; exists (yoneda_map X F).
unfold bijective, injective, surjective; split; simpl.
- intros S T Heq Y f.
generalize (natrans_naturality (IsNatrans:=S) f (Id X)); simpl.
rewrite cat_comp_id_dom; intros H; rewrite H; clear H.
generalize (natrans_naturality (IsNatrans:=T) f (Id X)); simpl.
rewrite cat_comp_id_dom; intros H; rewrite H; clear H.
now rewrite Heq.
- intros x.
exists (inv_yoneda_map X F x); simpl.
now rewrite (fmap_id (F:=F) X x).
Qed.同型射さえ構築できてしまえば、証明はなし崩し的に終わります。
以下に、同型を与える二つの射の定義を載せておきます。
Program Definition yoneda_map (C: Category)(X: C)(F: C --> Setoids)
: Map ((Setoids^C) Hom(X,-) F) (F X) :=
[ S in Natrans Hom(X,-) F :-> S X (Id X) ].Program Definition inv_yoneda_map (C: Category)(X: C)(F: C --> Setoids)
: Map (F X) ((Setoids^C) Hom(X,-) F) :=
[ x in F X :-> [ Y in C :=> [ f in C X Y :-> fmap F f x ]]].inv_yoneda_map の定義は、少々入れ子になっていてわかりづらいかもしれません。
F X から (Setoids^C) Hom(X,-) F への Map ということは、 x: F X を使って Hom(X,-) から F への自然変換を作ることになります。
Hom(X,-) から F への自然変換は、各対象 Y: C に対する Hom(X,Y) から (F Y) への Map の族から構築されているので、各 Map を [f :-> fmap F f x] として与えているわけです(fmap F f: Map (F X) (F Y) なので、 fmap F f x: F Y)。
自然変換の具体例として、 list や tree といった型変換子が函手をなし、その間の多相な函数が自然変換となっていることを見ていきます。
前回の記事(Coq で圏論：函手とその等価性) で option と list が 圏 Types 上の函手となっていることを見ました。
その定義を再掲しておきます。
Definition _option := option.
Program Definition option: Types --> Types :=
[Functor by f :-> option_map f].Definition _list := list.
Program Definition list: Types --> Types :=
[Functor by f :-> map f].また、今回、二分木を表わす型 tree X も次のように定義して、函手であることを述べておきます。
Inductive _tree (X: Type) :=
| leaf (x: X)
| node (tl tr: _tree X).
Fixpoint tree_map (X Y: Type)(f: X -> Y)(t: _tree X): _tree Y :=
match t with
| leaf x => leaf (f x)
| node tl tr => node (tree_map f tl) (tree_map f tr)
end.
Notation "[: x :]" := (leaf x).
Infix "-:-" := node (at level 50, left associativity).
Program Definition tree: Types --> Types :=
[Functor by f :-> tree_map f with X :-> _tree X].実際に自然変換の例を見ていきます。
option や list が Types 上の自己函手であったことから、もし存在するとすれば list から option への自然変換は X: Type に対する list X から option X への函数の族として与えらえるはずです。
そして、この「族」の型は forall X: Type, list X -> option X です。
実は、 Coq.Lists.List にこの型を持つものが定義されています。
リストの先頭の要素を取得する函数 hd_error です。
Definition hd_error (X: Type)(l: list X): option X :=
match l with
| [] => None
| x :: _ => Some x
end.そして、この hd_error が実際に自然変換になっていることを、次のようにして確かめることができます。
Program Definition hd_error_natrans: list ==> option :=
[X :=> @hd_error X].tree から list への自然変換として、二分木を平坦化する函数 tree_flatten を与えることができます。
Fixpoint tree_flatten (X: Type)(t: tree X): list X :=
match t with
| [:x:] => [x]
| tl -:- tr => tree_flatten tl ++ tree_flatten tr
end.
Program Definition tree_flatten_natrans: tree ==> list :=
[X :=> tree_flatten (X:=X)].また、少し特殊な例として length があります。
length の型は forall X: Type, list X -> nat です。
自然変換の値域として常に nat を返す定数函手を考えれば、これも自然変換になるのです。
Program Definition length_natrans: list ==> [* in Types |-> nat in Types] :=
[X :=> @length X].[* in Types |-> nat in Types] は見たまんま、 nat を返す Types から Types への定数函手です。
米田の補題とデータ型を同時に扱ってみましたが、ここでは関係ないんですよね。
Hom(X,-) が Setoids への函手なので、 Types とは相性がよくないのです。
ただ、 option や list や tree といったものたちからは Setoid が構成できるので、そうすれば関連を見出すことも可能です。
随伴からモナド作って、モナドから Kleisli triple でも作ってみましょうか。