Mercurial > hg > Papers > 2015 > atton-thesis

annotate category.tex @ 14:586f3ce1effe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add folding for section
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 08 Feb 2015 12:22:56 +0900
parents 11015b94a5cd
children 6c0d32ef01cd
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を用いて定義可能であることを示した。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
5 ここで Monad の定義と要請されるMonad則について述べる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
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}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
11 まずは Monad の定義に必要な Category (圏)について述べる。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
12
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
13 Category は2つの要素を持つ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
14
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
15 \begin{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
16 \item object (要素)
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
17
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
18 \item morphism (射, arrow)
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
19
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
20 object から object へのマッピング。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
21
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
22 morphism によってマップされる対象を domain と呼び、マップした先の対象を codomain と呼ぶ。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
23 つまり domain から codomain への object をマップするものが morphism である。
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
24 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
25
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
26 \begin{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
27 f : A \rightarrow B
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
28 \label{exp:morphism}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
29 \end{equation}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
30
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
31 \end{itemize}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
32
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
33
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
34
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
35 そして2つの法則を満たす。
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}
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
56 f : C \rightarrow D \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
57 g : B \rightarrow C \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
58 h : A \rightarrow B \nonumber \\
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
59 (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
60 \label{exp:morphism_composition_law}
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
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
94
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 \section{Functor}
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 \section{Natural Transformation}
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 \section{Monad}
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 \section{Monads in Functional Programming}
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99