自然変換
Menu Menu可換図
HomReasoning.agda 自然変換を理解すれば圏論は終わったようなものですが、さらっと可換とか書いてある割に良くわからないものです。そもそも自然変換とはなんなんのか? Agda を使うと理解できるようになるんでしょうか?自然変換は二つの Functor : A -> B に対して定義されます。ということは、二つの圏A,B が関係しています。以下の図が可換になると簡単に説明されているのが普通です。
F(f)
F(a) ---→ F(b)
| |
|t(a) |t(b) G(f)t(a) = t(b)F(f)
| |
v v
G(a) ---→ G(b)
G(f)
これは、可換あるいは可換図の定義だと思うべきです。図は人用のもので、Agda にとっては、 等式
G(f)t(a) = t(b)F(f)
だけが重要です。図と違って、こちらには F(a) が出て来ませんが、Agda で書くと暗黙の変数として、こそこそ書かれていることがわかります。Functor に習って自然変換の定義を以下のように書いてみます。
record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
( F G : Functor D C )
(TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
field
commute : {a b : Obj D} {f : Hom D a b}
→ C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ]
TMap が t(a) の t に相当します。
(TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
TMap は F(a) から F(b) への射を返すとういわけです。この→は写像で、TMap
一つの対象について、一つの射が対応する
という事を示しています。Hom C (FObj F A) (FObj G A)) はたくさんあるけど、そこから一つを選び出すわけです。例えば、Monoid では、対象は一つですが射はたくさんあります。
この等式 G(f)t(a) = t(b)F(f) は、どちらかといえば、
∀ G(f)t(a) = ∃ t(b)F(f)
と読むべきで、- 左回りの射の結合に対して、右回りの射がただ一つ決まる
Category では、
Functor は、List や Node という合成された型
Natural Transformation は、List 型の形の変換
と説明しています。List の形の変換は Haskell の関数そのものです。head や tail、flatten などです。これらが、自然変換なのは、
Functor の fmap と順序を換えて良い
からです。つまり、自然変換の可換性は、
fmap という合成された型の変換と、自分で書いた関数の可換性
でもあります。
t(a) のa は元の圏Aの対象で、t(a) 自体はFunctorの先の圏Bの射になっています。
プログラミングから見た自然変換
Functor はデータ型であり、その fmap はデータの構造を変えない、その中にある値の変換です。例えば、ファイルは行の集まりですが、その行は SJIS で書いてあるかも知れないし、UTF-8 で書いてあるかも知れません。SJIS から UTF-8 への変換はファイルに対する fmap (sjis->utf8) という形の変換です。例えば nkf -w は、そういう変換プログラムになります。nkf によるSJISからUTF-8の漢字コードの変換と、grep の順序を換えても良わけです。
nkf -w file | grep hoge == grep hoge file | nkf -w
みたいなものです。nkf は例えば、SJIS から UTF-8 にコード変換しますが、grep は検索する文字列が SJIS か UTF-8 を知る必要があります。つまり、grep (SJIS) とか grep (UTF-8) と書くべきです。
nkf -w file | grep (UTF-8) hoge == grep (SJIS) hoge file | nkf -w
この引数が t(a) t(b) に相当します。nkf は A(SJIS) から B(UTF-8) に変換する Funtor であり、grep は指定された型を扱う1行を取り出すというデータの形の変換です。
nkf -w
File(SJIJ) ------------→ File(UTF-8)
| |
|grep (SJIS) |grep (UTF-8)
| |
v v
Line(SJIS) ------------→ Line(UTF-8)
nkf -w
という可換性です。
これは、ファイルにはSJISであるかUTF-8であるかに関係ない構造があり、grep は、その構造にアクセスしていることを示してます。これは、nkf してから grep しても、grep してから nkf しても得られるものは同じ、つまり、同じプログラムだと思っても良いということです。
あるいは、UTF-8 のgrep を SJISの grep を nkf を使って実現することが可能だということでもあります。この図は UTF8 の grep を nkf を使って SJIS の grep に引っ張り出しているように見えます。自然変換は、このように、一つの射から同じ性質を持つ射を導くことに使うことができます。
良く出てくる自然変換
ここは飛ばしても良いです。後で出てくる自然変換を Agda で書いてみます。自然変換には二つの圏と二つのFunctorが関わりますが、その組み合わせにはいろいろあります。特に片方が identity Functor である場合が良く出てきます。Category の例を使います。
record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
( F G : Functor D C )
(TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
field
commute : {a b : Obj D} {f : Hom D a b}
→ C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ]
ですが Constructor としては、
record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′)
(F G : Functor domain codomain )
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
field
TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
isNTrans : IsNTrans domain codomain F G TMap
を使います。
まず、η : 1 -> T を調べます。
open import Category.Cat
postulate T : Functor A A
postulate η : NTrans A A identityFunctor T
identityFunctor は圏の圏 Category.Cat で定義されています。しかし、ここではあまり深く考えません。
record { FObj = λ x → x
; FMap = λ x → x
という定義だということだけを使います。自然変換の定義は以下の通りでした。
C [ C [ ( FMap G f ) o ( TMap μ a ) ] ≈ C [ (TMap μ b ) o (FMap F f) ] ]
record 外で呼ぶ時には、Tmap μ a と、μが入ります。FMap G は FMap T で、FMap F f は f なので、
C [ C [ ( FMap T f ) o ( TMap μ a ) ] ≈ C [ (TMap μ b ) o f ] ]
という形になります。自然変換の等式は様々な形で現れます。これを自分で見つけやすくするのが可換図の役割です。
自然変換の組み合わせ
Tη という、Functor T と η の組み合わせを考えます。
C [ C [ ( FMap T f ) o ( TMap μ a ) ] ≈ C [ (TMap μ b ) o f ] ]
の TMap μ a を FMap T ( TMap μ a ) するわけです。
C [ FMap T ( C [ ( FMap T f ) o ( TMap μ a ) ] ) ≈ FMap T ( C [ (TMap μ b ) o f ] ) ]
これに分配法則を使うと、
C [ C [ FMap T ( FMap T f )) o FMap T ( TMap μ a ) ] ≈ C [ (FMap T (TMap μ b ) o FMap T f ] ) ]
となります。これは、FMap T (TMap μ a ) が、FMap T f と FMap T (FMap T f) の自然変換になっているということです。FMap T (FMap T f ) はTを組み合わせた Functor で、T ○ T と書きます。この組み合わせも Cat.agda で定義されています。つまり、
Tη : NTrans A A T ( T ○ T )
ということです。これは、T と ηから新しい自然変換を得る演算だと考えることもできます。
逆に ηT を考えることもできます。今度は、TMap μ a の a に FObj T a 、f に FMap T f を入れます。
C [ C [ ( FMap T (FMap T f) ) o ( TMap μ (FObj T a) ) ] ≈ C [ (TMap μ (FObj T b) ) o FMap T f ] ]
TMap μ (FObj T a) が自然変換になっていることがわかります。
ηT : NTrans A A T ( T ○ T )
Tη も ηT も同じような組み合わせに見えますが、組み合わせ方はまったく異なります。
η : 1 -> T
があったら、
Tη : T -> ( T ○ T )
ηT : T -> ( T ○ T )
が定義できるというわけです。
自然変換の式では射の結合が出てくるので、結合する部分の Obj が対応する必要があります。
a -> b -> c
でなければなりません。自然変換には Obj の引数があり、自然変換の等式では、その引数の値が変わります。これを合わせるのはしんどい作業ですが、合ってなければ Agda が文句を言ってくれるのが救いです。
この演算を Agda で定義することもできます。
水平結合
自然変換同士を組み合わせることもできます。圏AからB、そしてCのような組み合わせは垂直結合と呼ばれれますが、水平結合と呼ばれる少し変わったものがあります。
postulate ε : NTrans A A ( T ○ T ) identityFunctor
があるとしましょう。TMap ε a は射なので、これに対してεの可換図を定義することができます。TMap ε a は、FObj T (FObj T a) から a への射です。
C [ C [ f o ( TMap ε a ) ] ≈ C [ (TMap ε b ) o (FMap T (FMap T f)) ] ]
の
f を TMap ε a に
a を FObj T (FObj T a) に
b を a に
置き換えます。
C [ C [ TMP ε a o ( TMap ε (FObj T ( FObj T a)) ) ] ≈ C [ (TMap ε a ) o (FMap T (FMap T (TMap ε a))) ] ]
これは、圏論の本では、
ε o ε T T = ε o T T ε
などと書かれます。自然変換が二つ続くのは珍しい。
本に現れる自然変換の式では、
εの直後のεTは、ε(T(a)) つまり、TMap ε (FObj T a)
εの直前のTεは、T(ε(a)) つまり、FMap T (TMap ε a)
o は射の結合
だというわけです。Functor T は Obj(対象) と Hom(射)の二種類の写像を持ち、本ではそれを Polymorhphic に使うわけです。しかし、Agda は Monomorphic なので、FObj と FMap と名前を変えることになります。それは、それでわかりやすいわけです。
圏論の計算に慣れると、 ε o εTT とかの式も当たり前に受け入れられるようになるのでしょう。