クライスリ圏

提供: miniwiki
移動先:案内、検索

圏論においてクライスリ圏（クライスリけん、英: Kleisli category）とは、『すべてのモナド[1]は関手の随伴対から得られるか』というP. J. Hiltonらの予想に対し、Heinrich Kleisliが解答をするにあたって導入した圏である[2]。

定義

クライスリトリプル（Kleisli triple）

圏 C 上のクライスリトリプル（Kleisli triple）とは、関手 T : C → C、自然変換 η（ηA : A → T A for A ∈ Obj(C)）、射 f : A → T B に対して射 f* : T A → T B を与える操作 _* からなる三つ組 （T, η, _*）で、以下

  • ηA* = 1T A
  • f*・ηA = f ただし、f : A → T B
  • g*・f* = (g*・f)* ただし、f : A → T B かつ g : B → T C

を満たすものを言う。

クライスリ圏（Kleisli category）

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

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

プログラムの圏としてのクライスリ圏（Kleisli category as category of programs）

計算機科学者のEugenio Moggiは、クライスリ圏の射をプログラム（program）に対応させる、すなわち射としてのプログラムが成す圏とはクライスリ圏であるとすることで表示的意味論にモジュール性を持たせることに成功した（モナドの理論）。

モナド則（Monad laws）

計算機科学者のPhillip Wadlerによってモナドの理論におけるクライスリトリプルにモナド則（Monad laws）という名称が与えられた。

合成順序が逆のときのクライスリトリプル

圏 C 上に定義された関手 T、自然変換 η、T への射に対する操作 _* が以下

  1. T A ; ηA*＝ T A[3]
  2. ηA ; f* ＝ f ただし、f : A → T B
  3. f* ; g* ＝ (f ; g*)* ただし、f : A → T B かつ g : B → T C

を満たすとき、三つ組（T, η, _*）をクライスリトリプルと呼ぶ。 

{-                     モナド則（Monad laws）                     -}
{- 右単位則（Right unit）　-}  T a `bindT` unitT == T a
{- 左単位則（Left unit）　 -}  (unitT a) `bindT` f == f
{- 結合規則（Associative）-}  T a `bindT` (\ x → (f x) `bindT` (\ y → g y) ) == (T a `bindT` (\x → f x) ) `bindT` (\y → g y)

脚注

  1. ↑ なお、モナド（余モナド）は当初、スタンダード構成（standard construction）と呼ばれていた。
  2. ↑ Kleisli(1965)
  3. ↑ モナド則との明白な対応関係をつけるため、元々の定義よりも冗長に記載した。簡潔に書こうと思えば
    ηA* ＝ 1T A
    で良い。

関連項目

参考文献



「http:///http:///mymemo.xyz/mymemo.xyz/wiki/index.php?title=クライスリ圏&oldid=106223」から取得