クライスリ圏

圏論においてクライスリ圏とは、『すべてのスタンダード構成は関手の随伴対から得られるか』という予想に対し、ハインリッヒ・クライスリが解答をするにあたって導入した圏である。

1. 概要
-----

スタンダード構成の概念はホモロジー代数の分野では早くから現れていたが、随伴概念の発見に伴い、すべてのモナドは関手の随伴対から得られるのではないかという予想がP.J.Hilton その他によって立てられていた。これに対し二つ解答が寄せられたが、その解答者の一人であるハインリッヒ・クライスリは『Every standard construction is induced by a pair of adjoint functors』で、

定理圏 L におけるスタンダード構成  が与えられたとする。このとき、圏 K が存在し、さらに  を導き随伴を成す二つの共変関手 F ： K → L と G ： L → K が存在する。を証明して解答したが、ここで新たに随伴対  を構成するために必要となるドメインの圏 K はクライスリ圏と呼ばれるようになった。クライスリ圏については、イタリアの計算機科学者エウジニオ・モッジによる計算機科学のプログラム意味論における応用がモナドの理論として存在する。

2. 定義
-----

2.1. クライスリトリプル
--------------

圏 C 上のクライスリトリプルとは、関手 T : C → C、自然変換 η、射 f : A → T B に対して射 f* : T A → T B を与える拡張演算子 _* からなる三つ組 で、以下

ηA* = 1T A
f*・ηA = f ただし、f : A → T B
g*・f* = * ただし、f : A → T B かつ g : B → T Cを満たすものを言う。

2.2. クライスリ圏
-----------

圏 C'// 上にクライスリトリプルが与えられているとき、////クライスリ圏'//CT とは、対象、射、射の合成規則を以下のとおり定めたものを言う。

CT の対象は、C の対象である
CT において、対象 A から B への射の集まり HomCT は、C における射の集まり HomC である
CT において、射 f ∈ HomCT と射 g ∈ HomCT の合成射とは、g*・f : A → T C である

3. モナドのクライスリ圏
-------------

圏 C 上のモナド <T,η,μ> が与えられたとすると、クライスリトリプルの拡張演算子 _*はモナドを用いて定義することができる。具体的には、任意の射 f : X → T Y に対して、_* を

とする。よって、モナド <T,η,μ> を与えることはクライスリトリプル を与えることと同値である。

4. 計算機科学における応用
--------------

計算機科学者のエウジニオ・モッジは、クライスリ圏の射をプログラムに対応させる、すなわち射としてのプログラムが成す圏とはクライスリ圏であるとすることで表示的意味論にモジュール性を持たせることに成功した。

4.1. プログラムの圏としてのクライスリ圏
----------------------

プログラミングの教則として、引数と返り値をもつことからプログラムとは数学の関数、すなわち集合写像であると教えられることがある。
しかしながらこの喩えは

入出力等をもたらすプログラム
例外を返すプログラム
引数に対して値を返さないプログラム
同じ引数でも返り値が異なる可能性のあるプログラムなどを説明することができない。つまり、プログラムは集合写像ではない。
プログラムの数学的モデルを見つけ出す過程において、モッジは圏論と表示的意味論の観点からプログラムは圏の射、型は圏の対象とみなすことができ、さらに直感的解釈として、関数が値を取り値を返すものであるのに対しプログラムが値を取り計算した 値を返す、すなわち引数の型と返り値の型の間にはなにか違いがあり単純な射の合成ができない、と考えた。

集合写像：値　→　　　　　　　値プログラム　　　：値　→　"計算した"　値モッジはこのような射としてのプログラムの数学的モデルとしてクライスリ圏の射が妥当であると主張し実際に副作用、例外処理、非決定計算などの効果をうまくクライスリ圏の枠組みで統一的に定式化できることを示した。その結果として伝統的な表示的意味論においては欠如していたモジュール性を付与することに成功した。

4.1.1. モッジの原理
-------------

理論的には、ある計算方式で"計算した"ことを示す印は、次のモッジの原理から型構築子として導入される。 特に、この計算方式を表す型構築子 T を計算概念と呼ぶ。

また、必然的に計算した値を返すプログラム概念は次のようになる。

モッジが主張するプログラムの概念型 A の引数を取り T の計算効果を伴いつつ計算をした型 B の値を返すプログラムとは、A → T Bの型を持つものである。この特徴付けによって、計算効果 T を伴うプログラムとなんら計算効果を持たない単なる集合写像は区別できるようになる。ただし、その代わりに２つのプログラムの合成を関数のように単純に行うことができなくなるのである。

例えば、program1 :: A → T B と program2 :: B → T C が与えられたとき、その合成を行おうと思っても、型 B というデータの型としての共通性はあっても計算概念の分だけ型に違いがあるため、実際にプログラムの合成を行うことはできない。

program2 :: B → T C × program1 :: A → T B この致命的な問題点を解消するために導入されるのがクライスリトリプルである。 直感的な記法となるが、クライスリトリプルが与えられれば、「_*」演算子の機能からprogram2* :: T B → T C となり

program2* . program1 :: A → T C という形でプログラムの合成が可能となる。おおよそこのような理由からモッジはプログラムはクライスリ圏をなすとした。

4.1.2. モナド則
-----------

プログラムの世界におけるクライスリ・トリプルに対応するものは、計算機科学者のPhillip Wadlerによって命名された次のモナド則である。 {- モナド則 -} {- 1.右単位則　-} T a `bindT` unitT == T a {- 2.左単位則　 -}  `bindT` f == f {- 3.結合規則-} T a `bindT`  `bindT`  ) ==  ) `bindT`  これに直接対応するのは次の合成順序を逆にしたのときのクライスリトリプルである。

4.1.3. クライスリ圏をなす計算概念の例
----------------------

クライスリ圏をなす計算概念としては以下の計算効果が挙げられる。

部分性T A = A⊥ηA は A から A⊥ の中への包含f : A -> T B であれば、f* = ⊥ 、f* = f ただし、a ∈ A非決定性T A = P//fin//ηA は単要素写像 a ↦ {a}f : A -> T B かつ c ∈ T A であれば、f* = ∪x ∈ cf副作用T A = SηA は写像 a ↦ f : A -> T B かつ c ∈ T A であれば、λs:S. in f)例外T A = A + EηA は入射写像 a ↦ inlf : A -> T B であれば、f*) = e  かつ f*) = f 継続T A = RηA は写像 a ↦ )f : A -> T B かつ c ∈ T A であれば、f* = ))

5. 脚注
-----

6. 参考文献
-------

7. 関連項目
-------

モナド 
モナド