米田の補題

米田の補題は、圏論の定理である。俗に「最も難しい自明な定理」と呼ばれる。

概要

圏論の世界においては自然変換と呼ばれる、ファンクター同士の間の関連性が重要な役割を果たす。

自然変換には課される制約が多く、いい加減に定義するとまず自然変換にはならないため、もともとかなり構造が限定されやすい。

ファンクターの中には、表現可能ファンクターと呼ばれる特別な種類のファンクターが存在し、圏論の様々な場所で扱いやすいファンクターとして振る舞う。

米田の補題というのは「表現可能ファンクターから一般のファンクターへの自然変換は明らかなものに限定される」という定理である。

表現可能ファンクターというのが何なのかというと、ある対象Aに対して、Hom(A, -) = (X ↦ Hom(A, X))と表せるファンクターのことである。Hom(A, X)というのはAからXへの射の集合なので、プログラミング言語で言う「関数型」とほとんど同じ意味である。米田の補題は、表現可能ファンクターがある種「御しやすい」ファンクターである、という主張である。

主張

正確な主張は以下の通り。

Cを局所的に小さな圏とする。ファンクターF: C→Setと対象A ∈ Ob(C)に対して、以下の自然同型が存在する。

Nat(Hom_C(A, -), F)≅FA

(Natは全ての自然変換の集まり。この場合は集合でもある。)

とりわけ重要なのがF=Hom_C(B, -)の場合で、この場合ざっくりと以下のような主張になる。(米田埋め込み)

「全てのX ∈ Ob(C)に対するHom_C(A, X) →Hom_C(B, X)」とHom_C(B, A)は同じ個数存在する。

さらにもっと直接役に立ちそうな主張を抜き出すと以下の通りになる。

全てのX ∈ Ob(C)に対してHom_C(A, X) ≅Hom_C(B, X)であるとき、A ≅ Bである。

つまりA ≅ Bを示すのにHom_C(A, X) ≅Hom_C(B, X)を示せばよくなる。一見複雑になってしまったように見えるが、後で示すように実はこれで単純になっている。表現可能ファンクターが扱いやすいことがここでも効いている。

具体例

説明のために前提条件などを省いたところがあるので、雰囲気を掴むため以外の読み方をするときは注意すること。

群

群Gを固定する。Gが作用する集合Xを任意に取る。またG自体にGが自然に作用するものとみなす。(つまり、g◦h = ghとする。)このとき、{GからXへの、作用を保つ関数} ≅ Xが成り立つ。つまり、関数の行き先を単位元についてだけ定めれば、残りの行き先は自動的に決まってしまう。

(具体的にCとして何を取っているのかというと、対象1個、射がGの元それぞれに対して存在する圏である。ファンクターC → SetがまさにGの作用する集合である。AはCの唯一の対象である。)

多相関数

以下のHaskellの関数を考える。

f :: (Int -> a) -> Maybe a

この関数としてありえそうなものはどのようなものがあるだろう？まず思いつくのは、常にNothingを返す関数である。

λg -> Nothing :: (Int -> a) -> Maybe a

他には、Maybe Int型の値を一つ決め打ちして、それに対してfmapを適用する関数である。

λg -> fmap g (Just 1) :: (Int -> a) -> Maybe a

米田の補題は、fとしてあり得るものはこれら2種類に限定されることを主張する。つまりMaybe Int型の値によって全てが決められてしまうのである。λg -> Nothingはλg -> fmap g Nothingと同じであることに注意。

応用例

(説明のために、本来確かめるべきところを省いたので、雰囲気を掴むため以外の読み方をするときは注意すること。)

この定理は応用例が肝心である。例えば以下のような応用があり、計算が楽になる。

カルテシアン閉圏(直積と指数対象がある圏)において、A^B×C≅(A^B)^Cを証明したいとする。素直に計算しても良いのだが、米田の補題を使うと任意の対象Xに対してHom(X, A^B×C)≅Hom(X, (A^B)^C)を証明すれば良くなり、こちらの方が楽である。

Hom(X, A^B×C)≅Hom(X×(B×C), A) (指数対象の定義から)

≅Hom(X×(C×B), A) (×の交換法則から)
≅Hom((X×C)×B, A) (×の結合法則から)
≅Hom(X×C, A^B) (指数対象の定義から)
≅Hom(X, (A^B)^C) (指数対象の定義から)

関連項目

• 圏論
• 関手
• モノイド
• モナド(数学)

---

以下の記述は、編集者が飽きたために内容が少ないです。 調べものなどの参考にはなりますが絶対的に内容が不足しています。加筆、訂正などをして下さる協力者を求めています。

1. 以下の記述はモナド(プログラミング)の一部として作成された内容を元にしています。
2. 結局、初版作成者が書いていて何が正しいのかよくわからなくなったので、内容を鵜呑みにしないようにしてください。

Operationalモナド

なんでもファンクターにしてしまえるCoYonedaというものがある。米田信夫という日本人が発見した「米田の補題」をもとに実装したものらしい。「米田の補題」は圏論の世界ではかなり有名な定理のようだ。

Freeモナドと合わせれば何でもモナドにすることができる。というふうにしか紹介されないが、Haskellでいうところの型クラス、Javaでいうところの型引数を一つ取るジェネリクスに限られるようだ。

ちまたにあるCoYonedaというものの説明はよくわからない記号だらけである。CoYonedaの説明は、ファンクターが作れるというだけで、実装について説明していることはほとんどない。

米田の補題

記号を用いずに説明したものは皆無なのだが、比較的記号の利用が控えめで図もついている記事として以下を挙げておく。ただし英文でしかも長文である。

• Understanding Yoneda

ここでは証明には立ち入らない(上記リンクでも完全な証明まではしていない)。

Yonedaはどうやってファンクターを作るかというと、

ある型(対象)Aから型Xへの関数(射)の集合を、ある型クラス F で修飾された X すなわち F_AX を "対象" として対応させて圏を構成すると、「その新しく出来た対象と対象間の射」への射(下図の⇒)はファンクター則を満たす。

↙↙↙	A	(A -> X) -> FAX
↓↓↓	A-> X ↓↓↓	⇒	⇒	FAX
A -> Y ↓↓↓	u ↓↓↓	↘		↓
f ◦ u ↓↓↓	X	↓	⇒	↓
↓↓↓	X -> Y ↓↓↓	↙		↓ FAX -> FAY
↘↘↘	f ↓↓↓			↓
⇓	Y			↓
⇒	⇒	⇒	⇒	FAY
		(A -> Y) -> FAY

Haskellの型の記法を借りざるを得ない上に少しそれを崩して利用するが、

Yoneda f a x = (a -> x) -> f x

functorExample `fmap` f = λ k →

CoYonedaは上記の矢印を反対向きにしたもの

CoYoneda f a x = f x -> (x -> a)

そのときふしぎな事が起こった

CoYoneda f a = (f x, x -> a)

どうやらCoYonedaは関数でなくても f x と x -> a の値の組でもいけるらしい。

このあたりの事情は調べてもよくわからなかったのだが、どうも(->)を関数とみることに関係しているらしく、上の式の f と下の式の f は意味が少し違うかも? というか、この部分が米田の補題そのものなのかもしれないがよくわからなかった。

経緯はどうあれファンクター則を満たせはそれはファンクターであることに変わりはない。ダックタイピング

それにしても a の「値」はどこに入っているんだろう?

fmap g (fx, h) = (fx, g ◦ h)

とすると、

fmap (λ x → x) (fx, h) = (fx, (λ x → x) ◦ h) = (fx, h)

fmap g (fmap k (fx, h)) = fmap g (fx, k ◦ h) = (fx, g ◦ k ◦ h)

= fmap (g ◦ k) (fx, h)

これをFreeモナドにしてflatMapできるか検証する。

Free x >>= f = Free (fmap (>>= f) x)
Pure x >>= f = f x

(fx, h) `flatMap` g = fmap (>>=g) (fx, h) = (fx, (>>=g) ◦ h)

Operationalモナドの何がいいのか

既に述べたように、モナドはunit()とflatMap()をモナド則を満たすように定義してはじめてモナドとなるのである。Operationalモナドの何でもモナドにできるという触れ込みはかなり誇大広告だと思うが、それでも型の条件さえ満たす関数を定義しさえすれば、モナド則を満たすunit()とflatMap()が自動的に定義されるというところではないかと思われる?

もっとも、プログラミング上有意義な型の条件を満たす関数を定義するのが簡単かどうかはまた別の問題であるが。

ファンクター・アプリカティブ

圏論側から関手という記事が出来たので、独立した記事にするのは見合わせ、しばらく当記事内に置いておくことにする。

ファンクター

ファンクター(functor)は関手と訳され、Wikipediaにも「関手は「圏の圏」における射と考えることもできる。」という説明がなされている。function(関数)と英語も日本語も似ていることから、圏を圏に変換する関数のようなものを想像してしまう人もいるのではないだろうか。

実際、関数のようなものなのだが、圏は対象(の集合)と射(の集合)をセットにした概念であることを思い出してほしい。

圏を圏に変換するということは、対象を対象に変換する関数と、射を射に変換する関数の2つが必要になるのである。

ファンクターの解説はたいていHaskell(もしくはScala)で書かれているが、HaskellやScalaの"Functor"と圏論のファンクターは少しずれている。上述のように圏論のファンクターは、「対象を対象に変換する関数」と「射を射に変換する関数」の組み合わせであり、HaskellやScalaの"Functor"もそのあたりを概ね踏襲しているが、以下が違う。

1. 許されるファンクターは「型たちのなす圏」から「型たちのなす圏」へのファンクターのみ。
2. 必ず型コンストラクターを挟む。
3. ファンクターの規則を強制する方法がないため、ファンクター則を満たさない"Functor"を定義することも可能ではある。"Functor"がファンクター則を満たすかどうかは実装者の良識や注意力次第である。

「対象を対象に変換する関数」以外に fmap という「射を射に変換する関数」が定義される。プログラミング上は「変換前の対象が引数と返り値である関数」を「変換後の対象が引数と返り値である関数」に変換する関数。function を map するからfmap なのか functor の map だから fmap なのか、 fmap の名前の由来を調べてもわからなかった。他の命名法をみるに後者なら mapF という名前になりそうな気がするので前者なのではないだろうか。

ファンクター則というものがある。これはfmap :: (a -> b) -> f a -> f bが以下を満たさなければならないという規則である。

(λ x → x) `fmap` functorExample = functorExample

g `fmap` (f `fmap` functorExample) = (g ◦ f) `fmap` functorExample 

(ここで、

• functorExample :: f a
• f :: a -> b
• g :: b -> c

である。)

g ◦ f は数学の関数合成の記号で、g ◦ f(x) = g(f(x))である。正式には"∘"なのだが表示されない環境があるようなので"◦"で記述する。

「射を射に変換する関数」という点を意識して書くと、以下のようになる。

λ functorExample →(λ x → x) `fmap` functorExample  = λ functorExample → functorExample( = λ x → x)

λ functorExample → g `fmap` (f `fmap` functorExample) = λ functorExample → (g ◦ f) `fmap` functorExample

これはさらに簡潔に以下のようにも書ける。

fmap (λ x → x) = λ x → x

fmap g ◦ fmap f = fmap (g ◦ f)

HaskellのFunctorの説明はこのような表記を用いている。

アプリカティブ

アプリカティブはアプリカティブファンクターとも言われる。「射を射に変換する関数」で変換された関数以外に、射自身を対象として変換したもの(および、それと同じ型を有するが、射自身を対象として変換することでは生成できない関数)を、変換された対象たちを引数に取る関数として適用することができる。

この記述の末尾付近では、リストをファンクターとして見た時に、複数の関数のリストというものが、上記の例として挙げられている。

アプリカティブ則というのがあり、ファンクター則に加えてさらにいくつかの規則に従わねばならない。

後日書くことになりそうな気がするが、書かない。