Coq で圏論:自然変換とデータ型

  • 0
    Like
  • 0
    Comment

    まとめ

    前提

    以下の記事を読んでおくとわかりやすいかもしれません。
    - Coq で圏論:背景と普遍性について
    - Coq で圏論:函手とその等価性

    証明は省略していますが、ほぼ全て rewrite です。

    自然変換

    定義

    二つの函手 $F, G: C \rightarrow D$ について、自然変換 $S: F \Rightarrow G$ とは、射の族 $S= [ S_X: D(F(X),G(X)) ]$ であって

    \forall f \in C(X,Y).\ S_Y \circ F(f) = G(f) \circ S_X
    

    を満たすもののことです。

    この条件を仕様として書き下した型クラス 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]).
    

    函手圏 Fun C D

    自然変換 $S: F \Rightarrow G$ は、 $C$ から $D$ への函手の間の変換だと見做すことができます。
    すると、 $C$ から $D$ への函手を対象とした圏 $D^C$ を構築することが出来ます。

    射としての自然変換の等価性は

    S = T \Leftrightarrow \forall X.\ S_X = T_X
    

    で定義します。この定義でもって 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.
    

    そして、 $S$ と $T$ の合成を $T \circ S := [T_X \circ S_X ]$ で、 $F$ 上の恒等自然変換を $Id_F := [Id_{F(X)}]$ で定めれば、圏を構成するための道具が揃います。

    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)という、圏論の基本登場人物がまとめて登場する定理なので、やっておくとこれまでの議論の確認になっていいのではないかな、と思い、やってみました。

    米田の補題は、通常の圏論であれば、集合の圏 $Sets$ への函手 $F: C \rightarrow Sets$ と対象 $X \in C$ について、

    Sets^C(C(X,-),F) \cong F(X)
    

    が成り立つ、というものです。
    ここで、 $Sets^C(C(X,-),F)$ は函手圏 $Sets^C$ の hom 集合なので、共変 hom 函手 $C(X,-)$ から函手 $F$ への自然変換全体のなす集合です。

    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)。

    データ型と自然変換

    自然変換の具体例として、 listtree といった型変換子が函手をなし、その間の多相な函数が自然変換となっていることを見ていきます。

    Types 上の函手たち

    前回の記事(Coq で圏論:函手とその等価性)optionlist が 圏 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].
    

    自然変換としての多相函数

    実際に自然変換の例を見ていきます。

    hd_error

    optionlistTypes 上の自己函手であったことから、もし存在するとすれば 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_flatten

    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 があります。
    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 とは相性がよくないのです。

    ただ、 optionlisttree といったものたちからは Setoid が構成できるので、そうすれば関連を見出すことも可能です。

    次回予告

    随伴からモナド作って、モナドから Kleisli triple でも作ってみましょうか。