Mercurial > hg > Papers > 2015 > atton-thesis
changeset 11:76ce5bb18092
Add Category definition
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 08 Feb 2015 11:53:19 +0900 |
| parents | c2dda6eeab57 |
| children | 11015b94a5cd |
| files | appendix.tex category.tex delta.tex introduction.tex |
| diffstat | 4 files changed, 81 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/appendix.tex Sat Feb 07 19:41:05 2015 +0900 +++ b/appendix.tex Sun Feb 08 11:53:19 2015 +0900 @@ -0,0 +1,1 @@ +% TODO: 実験環境
--- a/category.tex Sat Feb 07 19:41:05 2015 +0900 +++ b/category.tex Sun Feb 08 11:53:19 2015 +0900 @@ -1,6 +1,81 @@ \chapter{Categorical Definitions of Monad} +\label{chapter:category} + +\ref{chapter:delta}章ではプログラムの変更がメタ計算としてMonadを用いて定義可能であることを示した。 +ここで Monad の定義と要請されるMonad則について述べる。 +また、定義は Monad の解説に必要な部分についてのみ解説する。 \section{Category} +まずは Monad の定義に必要な Category (圏)について述べる。 + +Category は2つの要素を持つ。 + +\begin{itemize} + \item object (要素) + + \item morphism (射, arrow) + + object から object へのマッピング。 + + morphism によってマップされる対象を domain と呼び、マップした先の対象を codomain と呼ぶ。 + つまり domain から codomain への object をマップするものが morphism である。 + domain A と codomain B を持つ morphism f は式\ref{exp:morphism}のように書くこととする。 + + \begin{equation} + f : A \rightarrow B + \label{exp:morphism} + \end{equation} + +\end{itemize} + + + +そして2つの法則を満たす。 +\begin{itemize} + \item 全ての object について identity mapping が存在する + + identity mapping とは domain と codomain が同じ morphism のことである。 + identity mappping は id と略する。 + id は全ての object に存在するため、 object A に対する id は $ id_A $ と書く。 + なお、id は全ての object に存在するために省略して書くことが多い。 + + \item 同じ obejct が domain と codomain になっている2つのmorphismは合成することができ、合成の順番は結果に影響しない。 + + morphism の合成には記号 $ \circ $ を用いる。 + object B から C への morpshim f と object A から B への morphism g があった時、 f と g を合成すると式\ref{exp:morpshim_compose}となる。 + + \begin{equation} + f \circ g : A \rightarrow C + \label{exp:morphism_compose} + \end{equation} + + 改めて、morphism の合成の順序が結果に影響しないことを式にすると式\ref{exp:morphism_composition_law}のようになる。 + + \begin{eqnarray} + f : C \rightarrow D \nonumber \\ + g : B \rightarrow C \nonumber \\ + h : A \rightarrow B \nonumber \\ + (f \circ g) \circ h = f \circ (g \circ h) : A \rightarrow D + \label{exp:morphism_composition_law} + \end{eqnarray} +\end{itemize} + +例えば、object A,B と A から B への moprhism を持つ category は図\ref{fig:simple_category}のようになる。 + +% TODO: simple category figure + + +object を点、morphism を線とした図を commutative diagram (可換図式) と呼ぶ。 +ある object から object への morphism の合成の path に関わらず結果が同じである時、その図を commutative (可換)と呼ぶ。 +例えば、式\ref{exp:morphism_composition_law}の category の commutative diagram は図\ref{fig:morphism_composition_law}のようになる。 + +% TODO: morphism_composition_law + + +commutative diagram が commutative である時、moprhism の合成順序が異なっても結果が同じであることを利用して等価性の証明を行なうことを diagram chasing と呼ぶ。 +ある性質を category に mapping し、diagram chasing を用いて証明を導くことで性質を解析していく。 + + \section{Functor} \section{Natural Transformation} \section{Monad}
--- a/delta.tex Sat Feb 07 19:41:05 2015 +0900 +++ b/delta.tex Sun Feb 08 11:53:19 2015 +0900 @@ -1,4 +1,5 @@ \chapter{プログラムの変更を表現する Delta Monad} +\label{chapter:delta} 本研究では Monad によりプログラムの変更を定義する。 @@ -18,11 +19,11 @@ \section{Delta Monad の定義} -任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{meta_computation_definition}のように定義される。 +任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義される。 \begin{equation} T A = V A - \label{meta_computation_definition} + \label{exp:meta_computation_definition} \end{equation} V はプログラムの全てバージョンの集合であり、V AとすることでAに対応する値の集合を返すものとする。