Wikipedia

クライスリ圏

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

概要

編集

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

定理
圏 L におけるスタンダード構成 (C,k,p) が与えられたとする。このとき、圏 K が存在し、さらに (C,k,p) を導き随伴を成す二つの共変関手 F ： K → L と G ： L → K が存在する。

を証明して解答したが、ここで新たに随伴対 (F,G) を構成するために必要となるドメインの圏 K はクライスリ圏（Kleisli category）と呼ばれるようになった。クライスリ圏については、イタリアの計算機科学者エウジニオ・モッジによる計算機科学のプログラム意味論における応用がモナドの理論として存在する。

定義

編集

クライスリトリプル（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 を与える拡張演算子（extension operator） _* からなる三つ組 （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 である

モナドのクライスリ圏

編集

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

 

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

計算機科学における応用

編集

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

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

編集

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

  • 入出力等をもたらすプログラム
  • 例外を返すプログラム
  • 引数に対して値を返さない（停止しない）プログラム
  • 同じ引数でも返り値が異なる可能性のあるプログラム

などを説明することができない。つまり、プログラムは集合写像ではない（a program is NOT a mapping）[5]。
プログラム（program）の数学的モデルを見つけ出す過程において、モッジは圏論と表示的意味論の観点からプログラムは圏の射、型は圏の対象とみなすことができ[6]、さらに直感的解釈として、関数が値を取り値を返すものであるのに対しプログラムが値を取り計算した 値を返す[7][8]、すなわち引数の型と返り値の型の間にはなにか違いがあり単純な射の合成ができない、と考えた。

集合写像（関数）：値　→　　　　　　　値
プログラム　　　：値　→　"計算した"　値

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

モッジの原理（Moggi's principle）

編集

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

モッジの原理（Moggi's principle）[13][14]
計算によって得られた型 A の値（computations of type A）は、型 T A の値に対応する
（Computations of type A correspond to values of type T A.）

特に、この計算方式を表す型構築子 T を計算概念（a notion of computation）と呼ぶ[15]。

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

モッジが（暗黙的に）主張するプログラムの概念
型 A の引数を取り T の計算効果を伴いつつ計算をした型 B の値を返すプログラム（program）とは、
A → T B
の型を持つものである。

この特徴付けによって、計算効果 T を伴うプログラムとなんら計算効果を持たない単なる集合写像（関数）は区別できるようになる。ただし、その代わりに２つのプログラムの合成を関数のように単純に行うことができなくなるのである。

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

program2 :: B → T C × program1 :: A → T B （合成不可）

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

program2* . program1 :: A → T C （合成可能）

という形でプログラムの合成が可能となる。おおよそこのような理由からモッジはプログラムはクライスリ圏をなすとした[16]。

モナド則（Monad laws）

編集

プログラムの世界におけるクライスリ・トリプルに対応するものは、計算機科学者のPhillip Wadlerによって命名された次のモナド則（Monad laws）である。 

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

これに直接対応するのは次の合成順序を逆にしたのときのクライスリトリプルである。

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

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

  1. T A ; ηA*＝ T A（モナド則との明白な対応関係をつけるため、元々の定義よりも冗長にしてある。）
  2. ηA ; f* ＝ f ただし、f : A → T B
  3. f* ; g* ＝ (f ; g*)* ただし、f : A → T B かつ g : B → T C

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

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

編集

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

部分性（partiality）
T A = A⊥（= A + { ⊥ }）
ηA は A から A⊥ の中への包含（inclusion）
f : A -> T B であれば、f*(⊥) = ⊥ 、f*(a) = f(a) ただし、a ∈ A
非決定性（nondeterminism）[18]
T A = Pfin(A)
ηA は単要素（singleton）写像 a ↦ {a}
f : A -> T B かつ c ∈ T A であれば、f*(c) = ∪x ∈ cf(x)
副作用（side-effects）
T A = (A × S)S
ηA は写像 a ↦ (λs: S.<a,s>)
f : A -> T B かつ c ∈ T A であれば、λs:S.(let <a, s'> = c(s) in f(a)(s'))
例外（exceptions）[19]
T A = A + E
ηA は入射（injection）写像 a ↦ inl(a)
f : A -> T B であれば、f*(inr(e)) = e (ただし、e ∈ E) かつ f*(inl(a)) = f(a) (ただし、a ∈ A)
継続（continuations）
T A = R(RA)
ηA は写像 a ↦ (λk: RA. k(a))
f : A -> T B かつ c ∈ T A であれば、f*(c) = (λk: RB .c(λa: A.f(a)(k)))

脚注

編集
  1. ^ Kleisli(1965)
  2. ^ 大熊(1979) pp.205-207
  3. ^ Moggi(1991) p.3
    In order to justify the axioms for a Kleisli triple we have first to introduce a category CT whose morphisms correspond to programs.
    ※ここで圏 CT はクライスリ圏（定義1.3）
    他 蓮尾(2011)
  4. ^ 佐伯(2001) p.11
  5. ^ つまり、Set もしくは Ens の普通の射ではない。
  6. ^ Moggi(1989)a p.17
  7. ^ Moggi(1989)a p.17
    3.2.1 A justification for monads
    In order to justify the use of monads for modelling notions of computations we adopt the following intuitive understanding of programs: a program is a function from values to computations.
  8. ^ 圏論の創始者の一人のマックレーンの著作でも、圏Set（もしくは Ens） の普通の射に計算（computation）概念は全く含まれていないことが確認できる。形式と機能(1992) pp.163-173
  9. ^ Moggi(1989)a p.18
  10. ^ 計算効果（computational effects）と呼ばれる。Filinski(1994)、勝股(2011)
  11. ^ 例えば、デイビッド・エスピノーザによる、モナドを用いたモジュラーな意味論を採用することでレゴブロックを組み立てるように言語を組み立てることができることを実証などがある。Espinosa_draft(1995)
  12. ^ なお、モッジはプログラミング言語のML（MetaLanguage）のような型システムを持つ言語を前提に理論を展開している。
  13. ^ Filinski(1994) p.447
  14. ^ 参照
    1 A categorical semantics of computations
    The basic idea behind the categorical semantics below is that, in order to interpret a programming language in a category C, we distinguish the object A of values (of type A) from the object TA of computations (of type A), and take as denotations of programs (of type A) the elements of TA. In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion of computation, since it abstracts away from the type of values computations may produce. There are many choices for TA corresponding to different notions of computations.
    Moggi(1991) pp.2-3
  15. ^ Moggi(1991) p.3
  16. ^ Moggi(1989)a pp.17-18
  17. ^ Moggi(1991) pp.4-5
  18. ^ プログラミング言語のHaskellにおいてはリストモナドとして知られる。
  19. ^ HaskellにおいてはMaybeモナドとして知られる。inr(e) = Nothing、inl(a) = Maybe a

参考文献

編集

関連項目

編集
「https://ja.wikipedia.org/w/index.php?title=クライスリ圏&oldid=98965057」から取得