Mercurial > hg > Papers > 2015 > atton-thesis

annotate category.tex @ 50:37a832dff044

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add DeltaM example
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 15 Feb 2015 17:56:51 +0900
parents 113b49263d40
children bf136bd59e7a
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{Categorical Definitions of Monad}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
2 \label{chapter:category}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
3
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
4 \ref{chapter:delta}章ではプログラムの変更がメタ計算としてMonadを用いて定義可能であることを示した。
33
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
5 \ref{chapter:category}章では category により Monad の定義と要請されるMonad則について述べる。
113b49263d40 Split chapter to description monad. category/functional programming
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
6 定義は Monad の解説に必要な部分についてのみ解説する。
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
8 % {{{ Category
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
9
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 \section{Category}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
11 \label{section:category}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
12 まずは Monad の定義に必要な Category (圏)について述べる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
13
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
14 category は2つの要素を持つ。
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
15
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
16 \begin{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
17 \item object (要素)
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
18
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
19 \item morphism (射, arrow)
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
20
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
21 object から object へのマッピング。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
22
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
23 morphism によってマップされる対象を domain と呼び、マップした先の対象を codomain と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
24 つまり domain から codomain への object をマップするものが morphism である。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
25 domain A と codomain B を持つ morphism f は式\ref{exp:morphism}のように書くこととする。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
26
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
27 \begin{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
28 f : A \rightarrow B
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
29 \label{exp:morphism}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
30 \end{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
31
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
32 \end{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
33
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
34 そして category は object と moprhism に対して2つの法則を満たす。
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
35
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
36 \begin{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
37 \item 全ての object について identity mapping が存在する
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
38
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
39 identity mapping とは domain と codomain が同じ morphism のことである。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
40 identity mappping は id と略する。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
41 id は全ての object に存在するため、 object A に対する id は $ id_A $ と書く。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
42
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
43 \item 同じ obejct が domain と codomain になっている2つのmorphismは合成することができ、合成の順番は結果に影響しない。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
44
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
45 morphism の合成には記号 $ \circ $ を用いる。
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
46 object B から C への morpshim f と object A から B への morphism g があった時、 f と g を合成すると式\ref{exp:morphism_compose}となる。
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
47
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
48 \begin{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
49 f \circ g : A \rightarrow C
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
50 \label{exp:morphism_compose}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
51 \end{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
52
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
53 改めて、morphism の合成の順序が結果に影響しないことを式にすると式\ref{exp:morphism_composition_law}のようになる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
54
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
55 \begin{eqnarray}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
56 \label{exp:morphism_composition_law}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
57 f : C \rightarrow D \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
58 g : B \rightarrow C \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
59 h : A \rightarrow B \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
60 (f \circ g) \circ h = f \circ (g \circ h) : A \rightarrow D
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
61 \end{eqnarray}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
62 \end{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
63
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
64 例えば、object A,B と A から B への moprhism を持つ category は図\ref{fig:simple_category}のようになる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
65
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
66 \begin{figure}[htbp]
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
67 \begin{center}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
68 \includegraphics[scale=1.0]{fig/simple_category.pdf}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
69 \caption{object A,B と morpshim f を持つ category}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
70 \label{fig:simple_category}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
71 \end{center}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
72 \end{figure}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
73
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
74 なお、id は全ての object に存在するために省略して書くことが多いため、これからは省略する。
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
75
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
76 object を点、morphism を線とした図を commutative diagram (可換図式) と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
77 ある object から object への morphism の合成の path に関わらず結果が同じである時、その図を commutative (可換)と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
78 例えば、式\ref{exp:morphism_composition_law}の category の commutative diagram は図\ref{fig:morphism_composition_law}のようになる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
79
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
80 \begin{figure}[htbp]
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
81 \begin{center}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
82 \includegraphics[scale=0.8]{fig/morphism_composition_law.pdf}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
83 \caption{式\ref{exp:morphism_composition_law} の morphism の合成法則の category がなす commutative diagram}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
84 \label{fig:morphism_composition_law}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
85 \end{center}
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
86 \end{figure}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
87
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
88
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
89 commutative diagram が commutative である時、moprhism の合成順序が異なっても結果が同じであることを利用して等価性の証明を行なうことを diagram chasing と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
90 ある性質を category に mapping し、diagram chasing を用いて証明を導くことで性質を解析していく。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
91
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
92 % }}}
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
93
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
94 % {{{ Functor
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
95
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 \section{Functor}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
97 \label{section:functor}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
98 \ref{section:category} 節では category を定義した。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
99 \ref{section:functor} 節では category から category への mapping である Functor (関手)について解説する。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
100
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
101 functor F とはある category C から D への mapping である。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
102 functor F を用いて category C の object もしくは morphism である x を category D の object もしくは morphism に対応させることを式\ref{exp:apply_functor}のように記述する。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
103
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
104 \begin{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
105 F(x)
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
106 \label{exp:apply_functor}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
107 \end{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
108
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
109 functor は以下の functor 則を満たす。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
110
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
111 \begin{itemize}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
112 \item id を保存する
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
113
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
114 category C における object A への id $ 1_A $ は F A においても id として振る舞う。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
115
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
116 \begin{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
117 F(1_A) = 1_{F(A)}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
118 \end{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
119
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
120 \item morphism の合成を保存する
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
121
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
122 category C における morphism f g の合成を考える。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
123 合成された $ f \circ g $ を F により mapping することと、f と g を個別に F により mapping した後に合成した結果は同じである。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
124
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
125 \begin{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
126 F(f \circ g) = F(f) \circ F(g)
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
127 \end{equation}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
128 \end{itemize}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
129
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
130 functor の例を挙げる。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
131 まず、 3つの object A,B,C と morphism f,g,h を持つ category C を考える。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
132 category C の morphism は式\ref{exp:functor_categoryC}であるとする。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
133
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
134 \begin{eqnarray}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
135 \label{exp:functor_categoryC}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
136 f : A \rightarrow C \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
137 g : B \rightarrow B \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
138 h : B \rightarrow C \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
139 f = g \circ h
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
140 \end{eqnarray}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
141
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
142 次に、 2 つの object A', B' と morphism f', g' を持つ category D を考える。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
143 category D の morphism は式\ref{exp:functor_categoryD}であるとする。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
144
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
145 \begin{eqnarray}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
146 \label{exp:functor_categoryD}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
147 f : B' \rightarrow A' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
148 g : A' \rightarrow B' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
149 \end{eqnarray}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
150
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
151 C から D への functor F は式\ref{exp:functorF}のようなものがある。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
152
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
153 要素数が異なるため一見正しく mapping できないように思えるが、正しく Functor 則を満たしている。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
154
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
155 \begin{eqnarray}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
156 \label{exp:functorF}
15
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
157 F(A) = A' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
158 F(B) = B' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
159 F(C) = A' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
160 F(id_A) = F(id_{A'}) \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
161 F(id_B) = F(id_{B'}) \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
162 F(id_C) = F(id_{A'}) \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
163 F(f) = id_{A'} \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
164 F(g) = g' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
165 F(h) = f' \\ \nonumber
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
166 F(h \circ g) = F(h) \circ F(g) = f' \circ g' = id_{A'} = F(f)
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
167 \end{eqnarray}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
168
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
169 functor F を用いて category C を category D へと mapping した図が図\ref{fig:functor}である。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
170
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
171 \begin{figure}[htbp]
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
172 \begin{center}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
173 \includegraphics[scale=0.8]{fig/functor.pdf}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
174 \caption{Functor の例}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
175 \label{fig:functor}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
176 \end{center}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
177 \end{figure}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
178
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
179 functor により category から category への mapping を考えることが可能となった。
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
180
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
181 % }}}
6c0d32ef01cd Add Functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
182
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
183 % {{{ Natural Transformation
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
184
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 \section{Natural Transformation}
16
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
186 \label{section:natural_transformation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
187 \ref{section:functor}節では category から category への mapping である functor について述べた。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
188 \ref{section:natural_transformation}節では functor と functor の関係である Natural Transformation(自然変換)について述べる。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
189
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
190 category C から D への functor F, G が存在する時、F から G への変換 t を考える。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
191
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
192 t は category C の A に対し、F(A) から G(A) への変換を提供する(式\ref{exp:trans})。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
193
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
194 \begin{equation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
195 t(A) : F(A) \rightarrow G(A)
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
196 \label{exp:trans}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
197 \end{equation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
198
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
199 t が 式\ref{exp:natural_transformation}を満たす時、t を natural transformation を呼ぶ。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
200
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
201 \begin{eqnarray}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
202 \label{exp:natural_transformation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
203 f : A \rightarrow B \\ \nonumber
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
204 G(f)t(A) = t(B)F(f)
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
205 \end{eqnarray}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
206
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
207 t が natural transformation である時、 category A における A を functor F で移したのちに morphism を適用しても、 functor G で移した後に morphism を適用しても良いという可換性が得られる。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
208 式\ref{exp:natural_transformation}の可換図は図\ref{fig:natural_transformation}となる。
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
209
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
210 \begin{figure}[htbp]
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
211 \begin{center}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
212 \includegraphics[scale=1.0]{fig/natural_transformation.pdf}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
213 \caption{自然変換の可換図(式\ref{exp:natural_transformation})}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
214 \label{fig:natural_transformation}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
215 \end{center}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
216 \end{figure}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
217
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
218 % }}}
cff9f6f0ff25 Add description natural transformation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
219
17
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
220 % {{{ Monad
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
221
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
222 \section{Monad}
17
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
223 \label{section:monad}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
224 \ref{section:natural_transformation}節では functor 間の可換性 natural transformation について述べた。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
225
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
226 category, functor, natural transformation を用いて Monad を定義する。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
227
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
228 category C における monad とは以下の性質を持つ $ triple (T, \eta, \mu) $ である。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
229
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
230 \begin{itemize}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
231 \item $ T : C \rightarrow C $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
232
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
233 category C から C への functor T
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
234
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
235 \item $ \eta : id_C \rightarrow T $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
236
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
237 C から T への natural transformation $ \eta $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
238
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
239 \item $ \mu : T^2 \rightarrow T $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
240
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
241 $ T^2 $ から $ T $ への natural transformation $ \mu $
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
242
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
243 なお、 $ T^2 $ とは $ TT $ と同義であるとする。つまり functor T による mapping を2回行なうものである。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
244 回数を n 回とすることで $ T^n $ と記述する。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
245 \end{itemize}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
246
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
247 この $ triple (T, \eta, \mu) $ が図\ref{fig:monad_laws}の可換図を満たす。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
248 なお、Aに対する $ \mu $ を $ \mu_A $ と記述する。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
249 同じように A に対する $ \eta $ を $ \eta_A $ と記述する
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
250
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
251 \begin{figure}[htbp]
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
252 \begin{center}
20
beebe0ffbcad Fix figures
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
253 \includegraphics[scale=0.9]{fig/monad_laws.pdf}
17
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
254 \caption{$ triple (T, \eta, \mu) $ が Monad であるために満たすべき可換図}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
255 \label{fig:monad_laws}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
256 \end{center}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
257 \end{figure}
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
258
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
259 図\ref{fig:monad_laws} で示した可換図は monad が満たすべき Monad則であり、T に対する演算の可換性を強制する。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
260 $ \eta $ は T を1つ増やすオペレーションであり、$ \mu $ は T を 2 つから1つに減らすオペレーションである。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
261
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
262 左側の可換図は T が 3つある場合の可換性である。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
263 TTT に対して、 (TT)T のよう外側の2つのTに $ \mu $ を行なってから結果の TT に対して $ \mu $ を行なっても、 T(TT) のように内側の2つのTに $ \mu $ を行なってから結果の TT に対して $ \mu $ を行なっても可換であることを示す。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
264 つまり、TTTを減らす演算は左から行なっても右から行なっても良いことを示す。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
265
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
266 そして右側の可換図は T が1つである場合の可換性である。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
267 T A に対して $ \eta $ を行ない TT A としてから $ \mu $ を行なっても、T A の内部の A に対して $ \eta $ を行ない TT A としてか $ \mu $ を行なっても、 T A の id と同じであることを示している。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
268 つまり、Tに対する演算における左右の単位元となるような性質を $ triple (T, \eta, \mu) $ に強制することとなる。
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
269
e2afa8266ecc Add description Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
270 % }}}