--- a/bachelor_middle_draft/bachelor_middle_draft.tex	Sun Oct 26 22:10:43 2014 +0900
+++ b/bachelor_middle_draft/bachelor_middle_draft.tex	Sun Oct 26 23:38:29 2014 +0900
@@ -28,61 +28,71 @@
 
 % {{{ 研究目的
 
-\section{研究目的}
-プログラムを変更するとプログラムの実行内容も変更される。
+\section{研究目的と提案手法}
+プログラムを変更するとプログラムの実行結果も変化する。
 その際、変更前のプログラムでは正しく実行できていた内容が変更によって損なわれる場合がある。
-プログラムの変更を Monad によって行なうことにより、変更前のプログラムも保存しながらプログラムを変更する。
+プログラムの変更時に正しい実行結果が損なわれていないか自動で検知することを目的とする。
 
-さらに、プログラムの変更を Monad によって定義することにより、プログラムを変更することの意味や性質などを解析する。
+本研究では、自動で実行結果の変更を検知するために、プログラムの変更を Monad を利用して行なう。
+Monad を利用したプログラム変更の際、変更前のプログラムを保存しながら変更する。
+変更前のプログラムは保存されているので変更後も実行することができる。
+両方の実行結果を比較することにより実行結果が損なわれていないか検知する。
+
+また、プログラムの変更を Monad によって定義することによって、プログラムを変更することの意味や性質などを解析したい。
 
 % }}}
 
 % {{{ Monad
 
-\section{Monad}
-Monad とはプログラムのメタ計算に対応するもの\cite{moggi}である。
+\section{Haskell における Monad}
+Monad とはプログラムの型に対するメタ計算に対応するもの\cite{moggi}である。
 
-プログラムのデータは型に所属しており、関数は型から型への射と考える。
+プログラムのデータは型に所属しており、関数は型に所属する値を受けとって値を返すものとして考える。
 その際、任意の型Aを内包する型Tを定義することができる。
 型Aを内包した型Tを T A と記述する。
 
-特定の条件下において、型Aから型Bに変換する関数fを考えた時に、型 T A から型 T B に変換する関数 T f との対応が存在する。
-ここで、f を T f に変換する際に特定の計算を追加することができ、T の定義時に決めることができる。
-このことにより、型Aのデータに対して型Aから型Bに変換する関数fを適用するプログラムを、型T A のデータに対して型T Aから型T Bに変換する関数 T f のプログラムに変換することによって、変換前の処理に加えて型Tの定義時の計算を行なうことができる。
+ここで、型 T A の値と型Aから型T Bに変換する関数fをとり、型 T B の値を返す関数joinを定義することができる。
+関数join では関数f で行なわれる計算と join で行なわれる計算がある。
+計算の区別のために後者のことをメタ計算と呼ぶ。
+メタ計算は関数fの内容に関わらず、型Tの定義により決定する。
+このことにより、型Tに対するjoinを定義することで型Tに対するメタ計算を定義することが可能となる。
+型T Aの値に対し、任意の関数を適用する際にjoinを用いることで、関数適用時に型Tのメタ計算を毎回行なうことができる。
+このように、型Tに対してメタ計算を対応させたものがMonadである。
 
-この特定の条件がMonad則であり、Monad則を満たす型TをMonadと呼ぶ。
-Monadである型Tは変換前の計算に加えて型Tによって定義された計算を行なうことができる性質がある。
-型Tによって追加される計算部分をメタ計算として定義し、プログラム全体のデータと関数を Monad によって記述することによりメタ計算を関数適用時に実行する。
+型Aの値を型T Aの値に変更する関数と関数joinはMonad則\cite{monad-laws}(図\ref{haskell-monad-law})を満たす必要がある。
+プログラミング言語 Haskell においては型Aの値を型T Aの値に変更する関数名は return であり、joinは中置関数 \verb/>>=/ である。
+これらの関数2つがMonad則を満たす時、メタ計算と計算が正しく分離して行なれることが保証される。
 
 % }}}
 
 % {{{ Monad の定義
 
 \section{プログラムの変更を表現するMonad}
-プログラング言語HaskellではMonadは型に対する型クラスとして表現される。
-型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
-その関数群を満たした型Aを型クラスXのインスタンスであると言う。
-Monadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。
-
 プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。
 
 % {{{ Definiton Diff
 
 \begin{breakbox}
 \verb/ data Diff a = Diff [String] a [String] a/
-\caption{型変数を持つ型 Diff の定義}
+\caption{型変数を持つ型 Diff の定義(Haskell)}
 \label{diff-monad-definition}
 \end{breakbox}
 
 % }}}
 
-型変数aを持つ data 型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことによって構成される。
-このデータコンストラクタ Diff が型aの変数を型 Diff a に変換するTに相当している。
+型変数aを持つデータ型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことで構成される。
+このデータコンストラクタ Diff が型Aの変数を型 Diff A に変換するTに相当している。
 変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。
 文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。
-計算そのものに対しては影響しない。
+このリストはメタ計算にのみ利用される。
 
-型Diff を Monad のインスタンスとするために return と \verb/>>=/ を定義する(図\ref{diff-monad-instance-definition})。
+次にDiffをMonadとして定義する。
+HaskellではMonadは型に対する型クラスとして表現される。
+型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
+その関数群が定義された型Aを型クラスXのインスタンスであると呼ぶ。
+ある型を型クラスMonadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。
+
+型Diff に対して関数 return と \verb/>>=/ を定義する(図\ref{diff-monad-instance-definition})。
 % {{{ instance Monad Diff
 
 \begin{breakbox}
@@ -95,18 +105,18 @@
     return x = Diff [] x [] x
     d >>= f  = mu $ fmap f d
 \end{verbatim}
-\caption{Diff を Monad のインスタンスとして定義する}
+\caption{Diff を Monad のインスタンスとして定義する(Haskell)}
 \label{diff-monad-instance-definition}
 \end{breakbox}
 
 % }}}
 
-return はデータをMonadにするためのものであり、型aから型T aへの変換である。
-\verb/>>=/ は型aから型T bに変換するための関数を用いてT aから T b への変換を定義する。
-\verb/>>=/ によって計算が行なわれる際に型Diff が持っている2つ変数に対する計算を行なう。
-片方はプログラム変更前の値を持ち、もう片方は変更後の値を持つようにする。
+return はデータコンストラクタDiffによって型Aを型Diff Aへと変換する関数である。
+\verb/>>=/ では、メタ計算として型Diffが持っている2つ変数に対する計算を行なう。
+片方の変数はプログラム変更前の計算を行ない、もう片方は変更後の計算を行なうようにする。
+変更前の計算も行なうことで、変更前のプログラムの保存とする。
 
-また、型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることをAgdaによって証明した。
+また、型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることは定理証明支援系プログラミング言語Agdaによって証明済みである。
 
 % {{{ Monad-laws
 
@@ -166,7 +176,7 @@
 
 このプログラムの primeFilter 関数が返す Diff Monad を変更する。
 本来ならば素数である整数のみを返す計算だったが、変更により偶数である整数のみを返すようにした。
-変更後のプログラムを実行した例が図\ref{diff-result}である。
+図\ref{diff-program}のプログラムを実行した例が図\ref{diff-result}である。
 
 % {{{ results
 
@@ -197,10 +207,13 @@
     \item その個数を数えるために5となる
 \end{itemize}
 
-変更前の実行結果を保存しながらプログラムを変更し、新しい実行結果が得られた。
-今回は検証のために両方の実行順を評価した。
-しかし Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。
-よって、変更後のプログラムのみを計算する場合は変更前の計算は行なわれない。
+変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。
+この実行結果を比較することにより、変更前のプログラムの実行結果が損なわれていないか検知する。
+
+今回は検証のために変更前と変更後の両方のプログラムを実行した。
+しかし、必ず両方実行しなくてはならない訳では無い。
+Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。
+そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。
 遅延評価とDiff Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。