Binary file bachelor_middle_draft.pdf has changed

--- a/bachelor_middle_draft.tex	Tue Oct 28 17:28:21 2014 +0900
+++ b/bachelor_middle_draft.tex	Tue Oct 28 18:23:36 2014 +0900
@@ -35,33 +35,31 @@
 
 本研究では、自動で実行結果の変更を検知するために、プログラムの変更を Monad を利用して行なう。
 Monad を利用したプログラム変更の際、変更前のプログラムを保存しながら変更する。
-変更前のプログラムは保存されているので変更後も実行することができる。
+変更前のプログラムは保存されているため、変更後も変更前のプログラムとして実行することができる。
 両方の実行結果を比較することにより実行結果が損なわれていないか検知する。
 
-また、プログラムの変更を Monad によって定義することによって、プログラムを変更することの意味や性質などを解析したい。
+また、プログラムの変更を Monad によって定義することによって、プログラムを変更することの意味や性質などを解析する。
 
 % }}}
 
 % {{{ Monad
 
 \section{Haskell における Monad}
-Monad とはプログラムの型に対するメタ計算に対応するもの\cite{moggi}である。
+Monad とは(TODO:どうしよう)である\cite{moggi}。
+Monad の利用例としてプログラミング言語Haskellがある。
+HaskellにおいてMonadはプログラムの型に対するメタ計算に対応するものである。
 
-プログラムのデータは型に所属しており、関数は型に所属する値を受けとって値を返すものとして考える。
+Haskell においてプログラムのデータは型に所属しており、関数は型に所属する値を受けとって値を返すものである。
 その際、任意の型Aを内包する型Tを定義することができる。
 型Aを内包した型Tを T A と記述する。
 
 ここで、型 T A の値と型Aから型T Bに変換する関数fをとり、型 T B の値を返す関数joinを定義することができる。
-関数join では関数f で行なわれる計算と join で行なわれる計算がある。
+関数join内では関数f の計算と join で行なわれる計算の2つがある。
 計算の区別のために後者のことをメタ計算と呼ぶ。
 メタ計算は関数fの内容に関わらず、型Tの定義により決定する。
 このことにより、型Tに対するjoinを定義することで型Tに対するメタ計算を定義することが可能となる。
 型T Aの値に対し、任意の関数を適用する際にjoinを用いることで、関数適用時に型Tのメタ計算を毎回行なうことができる。
-このように、型Tに対してメタ計算を対応させたものがMonadである。
-
-型Aの値を型T Aの値に変更する関数と関数joinはMonad則\cite{monad-laws}(図\ref{haskell-monad-law})を満たす必要がある。
-プログラミング言語 Haskell においては型Aの値を型T Aの値に変更する関数名は return であり、joinは中置関数 \verb/>>=/ である。
-これらの関数2つがMonad則を満たす時、メタ計算と計算が正しく分離して行なれることが保証される。
+このように、型Tに対してメタ計算を対応させたものがHaskellにおけるMonadである。
 
 % }}}
 
@@ -89,7 +87,7 @@
 次にDiffをMonadとして定義する。
 HaskellではMonadは型に対する型クラスとして表現される。
 型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
-その関数群が定義された型Aを型クラスXのインスタンスであると呼ぶ。
+その関数群が定義された型Aを型クラスXのインスタンスと呼ぶ。
 ある型を型クラスMonadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。
 
 型Diff に対して関数 return と \verb/>>=/ を定義する(図\ref{diff-monad-instance-definition})。
@@ -116,7 +114,9 @@
 片方の変数はプログラム変更前の計算を行ない、もう片方は変更後の計算を行なうようにする。
 変更前の計算も行なうことで、変更前のプログラムの保存とする。
 
-また、型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることは定理証明支援系プログラミング言語Agdaによって証明済みである。
+なお、関数returnと \verb/>>=/ はMonad則\cite{monad-laws}(図\ref{haskell-monad-law})を満たす必要がある。
+これらの関数2つがMonad則を満たす時、メタ計算と計算が正しく分離して行なれることが保証される。
+型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることは定理証明支援系プログラミング言語Agdaによって証明済みである。
 
 % {{{ Monad-laws
 
@@ -224,14 +224,15 @@
 
 今後の課題としては大きく2つある。
 変更の個数の拡張と Monad によってプログラムを変更することの意味を調べることである。
+
 現状の Diff Monad はプログラムの変更を1つまでしか持つことができない。
-変更を無限回行なえるDiffを定義することで、プログラムに対する変更をMonadによる変更のみで表したい。
+変更を無限回行なえるDiffを定義することで、プログラムに対する変更をMonadによる変更のみで表現する。
 
-また、プログラムに対する変更がMonadによって表される場合、圏論の視点からどのような意味が捉えられるか調査したい。
+また、プログラムに対する変更がMonadによって表される場合、圏論の視点からどのような意味が捉えられるか調査する。
 Monadは圏論から導入された概念であり、プログラム側のMonadと圏論側のMonadは対応している。
 Diff Monad を圏論の観点で捉えることにより、Diff Monadの性質などを圏論側から導出できないかといった狙いがある。
 
-ひいては、プログラムを作ることや変更することは理論的にどのような意味を持つのかを探っていきたい。
+ひいては、プログラムを作ることや変更することは理論的にどのような意味を持つのかを探る。
 
 % }}}