--- a/paper/agda.tex	Tue Feb 17 17:48:30 2015 +0900
+++ b/paper/agda.tex	Wed Feb 18 11:10:19 2015 +0900
@@ -37,8 +37,7 @@
 \end{eqnarray}
 
 式\ref{exp:a_implies_b}のように A を仮定して B を導くことができたとする。
-この時 A は alive な仮定である。
-証明された B は A の仮定に依存していることを意味する。
+この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。
 
 ここで、推論規則により記号 $ \Rightarrow $ を導入する。
 
@@ -52,9 +51,9 @@
     \UnaryInfC{$ A \Rightarrow B $}
 \end{prooftree}
 
-そうすると、仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
+$ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
 A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
-このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導くことができる。
+このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
 なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。
 
 alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。
@@ -184,7 +183,7 @@
 \end{itemize}
 
 例として、natural deduction で三段論法を証明する。
-なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示すこととする。
+なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示す。
 
 \begin{prooftree}
     \AxiomC{ $ [A] $ $_{(1)}$}
@@ -337,7 +336,7 @@
 式の型に対する定義を正しく行なうことで証明を与える。
 
 $ \Rightarrow \mathcal{E} $ に対応する \verb/->E/ は関数の適用なので、値a と関数 f を受けとって適用することで B が得られる。
-なお、仮定を alive のまま証明を記述するのは依存した仮定を残すことになるため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。
+なお、仮定を alive のまま証明を記述するのは依存した仮定を残すため、必要な仮定を引数として受けとったり、implicit な parameter として指定して証明するのが良い。
 
 また、Agda は証明に用いる規則なども Agda 内部で定義することができる。
 例えば、直積型の定義はリスト\ref{src:product}のようなものがある。
@@ -435,8 +434,8 @@
     \lstinputlisting[label=src:three_plus_one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/three_plus_one.agda}
 \end{table}
 
-3+1 という1つの関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。
-そして証明を関数の定義として記述する。
+3+1 という関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。
+そして証明すべき式を関数の定義として記述する。
 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。
 
 $ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。

--- a/paper/bibliography.tex	Tue Feb 17 17:48:30 2015 +0900
+++ b/paper/bibliography.tex	Wed Feb 18 11:10:19 2015 +0900
@@ -1,7 +1,7 @@
 % 参考文献
 \def\line{−\hspace*{-.7zw}−}
 
-\nocite{git, hg, agdawiki}
+\nocite{git, hg, agdawiki, opac-b1092711, BarrM:cattcs}
 
 \bibliographystyle{jplain}
 \bibliography{reference}

--- a/paper/category.tex	Tue Feb 17 17:48:30 2015 +0900
+++ b/paper/category.tex	Wed Feb 18 11:10:19 2015 +0900
@@ -2,8 +2,8 @@
 \label{chapter:category}
 
 \ref{chapter:delta}章ではプログラムの変更がメタ計算としてMonadを用いて定義可能であることを示した。
-\ref{chapter:category}章では category により Monad の定義と要請されるMonad則について述べる。
-定義は Monad の解説に必要な部分についてのみ解説する~\cite{opac-b1092711}~\cite{BarrM:cattcs}。
+\ref{chapter:category}章では category による Monad の定義と要請されるMonad則について述べる。
+定義は Monad の解説に必要な部分についてのみ解説する。
 
 % {{{ Category
 
@@ -71,7 +71,7 @@
     \end{center}
 \end{figure}
 
-なお、id は全ての object に存在するために省略して書くことが多いため、これからは省略する。
+なお、id は全ての object に存在するために省略して書く。
 
 object を点、morphism を矢印とした図を commutative diagram (可換図式) と呼ぶ。
 ある object から object への morphism の合成の path に関わらず結果が同じである時、その図を commutative (可換)と呼ぶ。
@@ -86,7 +86,7 @@
 \end{figure}
 
 
-commutative diagram が commutative である時、morphism の合成順序が異なっても結果が同じであることを利用して等価性の証明を行なうことを diagram chasing と呼ぶ。
+commutative diagram が commutative である時、morphism の合成順序の可換性を用いて等価性の証明を行なうことを diagram chasing と呼ぶ。
 ある性質を category に mapping し、diagram chasing を用いて証明を導くことで性質を解析していく。
 
 % }}}
@@ -241,7 +241,7 @@
         $ T^2 $ から $ T $ への natural transformation $ \mu $
 
         なお、 $ T^2 $ とは $ TT $ と同義であるとする。つまり functor T による mapping を2回行なうものである。
-        回数を n 回とすることで $ T^n $ と記述する。
+        Tの数が n である時  $ T^n $ と記述する。
 \end{itemize}
 
 この $ triple (T, \eta, \mu) $ が図\ref{fig:monad_laws}の可換図を満たす。

--- a/paper/functional_programming.tex	Tue Feb 17 17:48:30 2015 +0900
+++ b/paper/functional_programming.tex	Wed Feb 18 11:10:19 2015 +0900
@@ -11,9 +11,7 @@
 \ref{section:monad}節では Monad の定義について述べた。
 \ref{section:category_in_program}節はプログラムと category の対応について述べる。
 
-プログラムには値と関数のみが存在する。
-
-任意の値は型付けられるとする。
+プログラムは値と関数のみで表され、型付けられる。
 変数x が型 A を持つ時、式\ref{exp:value_in_program}のように記述する。
 
 \begin{equation}
@@ -29,8 +27,8 @@
     f : A \rightarrow B
 \end{equation}
 
-そして、引数と返り値の型が等しい関数は関数結合できるとする。
-関数結合の記号には $ \circ $ を用いる。
+そして、ある関数fの引数の型と、ある関数g の返り値の型が等しいとき f と g は合成できる。
+関数合成の記号には $ \circ $ を用いる。
 例えば、 A を取り B を返す関数 f と、 B を取り C を返す関数 g の合成は式\ref{exp:function_compose_in_program}のようになる。
 
 \begin{eqnarray}
@@ -72,10 +70,7 @@
 
 プログラムにおけるfunctor は型引数を持つことのできるデータ型に対応する。
 型引数を持つデータ型とは、任意のデータ型に対して構成可能なデータ構造であり、List などが相当する。
-
-たとえば、List は数値の List であっても Bool の List であっても構成可能である。
-この List を、型を受けとり型を返す型であると考えると、渡す型が引数のように振る舞う。
-この引数が型引数である。
+List を型を受けとり型を返す型であると考えると、渡す型が引数のように振る舞うため型引数と呼ばれる。
 
 \begin{eqnarray}
     \label{exp:functor_type}
@@ -93,14 +88,14 @@
 \end{table}
 
 functor であることを保証したい型は f として表される。
-そしてデータ型が functor であることを示すためには、 fmap という関数を定義すれば良いことが分かる。
+型クラスの定義から、f において fmap 関数を定義することで Functor となる。
 fmap は型a から型bへの関数を取り、f a を取り f b を返す。
 つまり、f でない型への演算をfの型においても適用するために変換する関数である。
 プログラムにおいて morpshim は関数であるため、fmap は $ A \rightarrow B $ の morphism を $ F A \rightarrow F B $ へと mapping する役割を担っている。
 なお、 fmap の型を \verb/ fmap :: (a -> b) -> ((f a) -> (f b))/ と読むことで、関数を受けとりfにおける関数に変換していることが分かりやすくなる。
 
 また、fmap の型に $ f a $ が存在するように、 f は型を引数として受けとっている。
-ここで object は型であるため、 $ A $ の object を $ F(A) $ への mapping する役割をf が担っていることが分かる。
+ここで object は型であるため、 $ A $ の object を $ F(A) $ への mapping する役割をf が担う。
 よって型引数を持つ型f と対応する fmap を定義することにより functor が定義できる。
 
 functor の例として、型がInt である変数 x と Int から Bool を返す even 関数を考える。
@@ -109,13 +104,12 @@
 
 例えば List がなす category Dがある。
 
-まずHaskell において List を定義する。
-List は任意の型 a を取り、 List a とする。
-空の List は Nil とし、List a に対して a の値を Cons で追加することによって List を構築するとする。
+まずHaskell においてデータ型 List を定義する。
+空の List は Nil とし、List a に対して a の値を Cons で追加することで List を構築する。
 
-ここで List が Functor であると定義する。
+ここで List が Functor とするために、 fmap を考える。
 fmap は a を取りbを返す関数を取り、List a を取って List b を返す関数である。
-つまり、関数を取ってList の全ての要素に適用することで実現できる。
+よって、関数を取ってList の全ての要素に適用することで実現できる。
 
 定義した結果がリスト\ref{src:list_in_haskell} である。
 
@@ -156,7 +150,7 @@
 \end{table}
 
 1行目がid の保存に、2行目が関数の合成の保存に対応している。
-なお、 Haskell における関数合成は \verb/./ によって行なわれる。
+なお、 Haskell における関数合成は中置関数 \verb/./ により行なわれる。
 
 % }}}
 
@@ -174,7 +168,7 @@
 つまりある functor f と g があった時に、 f において morphism を適用してtを適用しても、t を適用してから g において morphism を適用しても結果が変わらないような t を提供できれば良い。
 
 プログラムにおける natural transformation t は図\ref{fig:natural_transformation}を満たすような関数として表現される。
-Haskell において特定の関数が持つ性質を制約として記述することはできないため、Haskell において natural transformation の具体的な定義は存在しない。
+Haskell において特定の関数が持つ性質を制約として記述することはできないため、natural transformation の具体的な定義は存在しない。
 
 List における natural transformation の例としては、List の先頭を除いた List を返す tail 関数がある(\ref{src:natural_transformation_in_haskell})。
 tail 関数を Functor List から Functor List への natural transformation とみなすのである。
@@ -226,7 +220,7 @@
 T は functorであり、$ \eta $ は $ A \rightarrow T A $ 、 $ \mu $ は $ T^2 A \rightarrow T $ の natural transformation であった。
 
 Haskell において functor は型引数を持つ型とfmapで表現され、 natural transformation は図\ref{fig:natural_transformation}の可換図を満たす関数であった。
-つまり、型と fmap、2つの関数を適切に定義することによって表現される。
+つまり、 triple を表現するには 型Tと fmap、$ \eta $ と $ \mu$ の定義することになる。
 
 Haskell において、 $ \eta $ と $ \mu $ の型は以下のようになる。
 
@@ -253,7 +247,7 @@
 List において非決定性を表現する時、$ \eta $ は値から長さ1の List を構築する関数、 $ \mu $ は List の List から List を返す concat 関数となる。
 
 この $ \eta $ と $ \mu $ を用いて非決定性を表現する。
-List a はありうる値の集合であるとする。
+List a はありうる値の集合である。
 関数は値を取り、値から取りうる値をList として返す。
 この関数を List a に対して fmap することで、ありうる値に対して全ての取りうる値を計算することができる。
 この際、 List a に対して a から List a を返す関数を適用するために List a を持つ List が構築される。
@@ -287,7 +281,7 @@
 
 先程述べたように、 $ \eta $ は値を List とする関数、 $ \mu $ はList を内包する List を全て結合する関数である。
 
-この List Monad を実行する。
+この List Monad を実行した例を述べる。
 まずはありうる値のリストとして100, 200, 400 を持つ List の x を考える。
 次に、値から取りうる計算結果を返す関数として f を定義する。
 取りうる計算結果として、1加算した結果、10加算した結果、2乗した結果が存在するとし、結果は List として返す。

Binary file paper/main.pdf has changed

--- a/paper/main.tex	Tue Feb 17 17:48:30 2015 +0900
+++ b/paper/main.tex	Wed Feb 18 11:10:19 2015 +0900
@@ -23,7 +23,6 @@
 %   卒論の修正点
 %       実行例で Delta を使わないのも出す
 %       可能な変更の一覧
-%       留意して欲しいって論文っぽくない
 
 
 %%

--- a/paper/proof_delta.tex	Tue Feb 17 17:48:30 2015 +0900
+++ b/paper/proof_delta.tex	Wed Feb 18 11:10:19 2015 +0900
@@ -3,7 +3,7 @@
 第\ref{chapter:agda}章では Agda における証明手法について述べた。
 第\ref{chapter:proof_delta}章では Agda を用いて Delta Monad が Monad であることを証明していく。
 証明のゴールは Delta Monad が Funcor 則と Monad 則を満たすことの証明である。
-なお、証明は全ての Delta が同じバージョンを持つという制約下において成り立った。
+なお、証明は全ての Delta が同じバージョンを持つという制約下で行なった。
 
 % {{{ Agda における Delta Monad の表現
 
@@ -68,9 +68,8 @@
 record Functor が取る F は Set l を取り Set l を取る関数である。
 Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。
 よって、プログラムの level l を取り、変更せずに level l の Set を返すようにする。
-それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。
-よって suc により level を一段上げる。
-これは、証明の対象となるプログラムと証明そのものを混同しないためである。
+それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムでは無い。
+これは、証明の対象となるプログラムと証明そのものを混同しないために、 Functor の Level を suc により上げる。
 
 record Functor の field には以下のようなものがある。
 
@@ -117,9 +116,9 @@
 関数 f は型 A から B への関数とし、 Delta A から Delta B への関数に mapping する。
 コンストラクタ2つのパターンマッチを使って再帰的に f を delta の内部の値への適応することで fmap を行なう。
 
-データ型Delta と関数fmap を定義できたので、これらが Functor 則を満たすか証明していく。
+定義した データ型Delta と関数fmap が Functor 則を満たすか証明していく。
 なお、今回 Delta は全ての場合においてバージョンを1以上持つものとする。
-その制約は引数の Delta のバージョンに必ず S を付けることで1以下の値を受けつけないようにすることで行なう。
+その制約は引数の Delta のバージョンに必ず S を付けることで行なう。
 
 
 \begin{itemize}
@@ -180,7 +179,7 @@
 そのためまず要素として $ T $ , $ \eta $, $ \mu $ が存在する。
 T は Set l を取り Set l を返す型であり、Functor則を満たす。
 $ \eta $ は T を増やす関数であり、 $ \mu $ は T を減らす関数である。
-これら Monad の構成要素を定義する field である。
+これらが Monad の構成要素を定義する field である。
 
 次に、$ \eta $ と $ \mu $ は natural transformation である必要がある。
 よって field に制約として $ \eta $ と $ \mu $ の natural transformation を定義する。
@@ -211,7 +210,7 @@
 さらに、バージョンはプログラム全体で1以上の値を持ち、プログラム内で統一されるものとする。
 
 まず、リスト\ref{src:delta_instance_monad} で示した Delta Monad のメタ計算を Agda で再定義する(リスト\ref{src:delta_monad_in_agda})。
-Haskell での定義は Kleisli Trple による定義であるため、リスト\ref{src:monad_and_bind}で示した Kleisli Triple と Monad の対応を用いて定義していることに留意する。
+Haskell での定義は Kleisli Trple による定義であるため、リスト\ref{src:monad_and_bind}で示した Kleisli Triple と Monad の対応を用いて変形している。
 
 \begin{table}[html]
     \lstinputlisting[label=src:delta_monad_in_agda, caption=Agdaにおける Delta に対する Monad の定義] {src/delta_monad_in_agda.agda.replaced}
@@ -219,16 +218,15 @@
 
 
 $ \eta $ に相当する delta-eta はメタ計算における T を1つ増やす演算に相当する。
-内包する値のバージョンに依存して Delta が持つバージョンが決まるため、 Nat の値によりバージョン数を決められるようにしておく。
-なお、パターンマッチの項に存在する \verb/{}/ は、 implicit な値のパターンマッチに用いられる。
+内包する値のバージョンに依存して Delta が持つバージョンが決まるため、 Nat の値によりバージョン数を決める。
+なお、パターンマッチの項に存在する \verb/{}/ は、 implicit な値のパターンマッチである。
 例えば \verb/{n = S x}/ とすれば、 implicit な値 n は S により構成される時にこの定義が実行され、S を省いた残りの値は x に束縛される。
 
 次に $ \mu $ に相当する delta-mu を定義する。
-delta-mu は複数の \verb/TT -> T/に対応するメタ計算であるため、1段ネストされた Delta を受けとり、Deltaとして返す。
+delta-mu は複数の \verb/TT -> T/に対応するメタ計算であるため、 Delta Delta を受けとり、Deltaを返す。
 これはバージョン管理された値に対し、バージョン管理された関数を適用した場合の値の選択に相当する。
-例えばバージョンが5であった場合、全ての組み合せは5パターン存在する。
-その中から5つを選ぶルールとして $ \mu $ を定義する。
-$ \mu $ は値と関数が同じバージョンであるような計算結果を選ぶように定義する。
+$ \mu $ は値と関数が同じバージョンであるような計算結果を返す。
+例えば関数と値のバージョンがそれぞれ5である時、全ての組み合せは25パターンの中から5パターンを返す。
 
 同じバージョンである値を選ぶため、先頭のバージョンの値を取る headDelta 関数と、先頭以外のバージョン列を取る tailDelta 関数を用いている。
 
@@ -245,7 +243,7 @@
 
 
         \lstinputlisting[label=src:delta_eta_is_nt_in_agda,
-                        caption= Agda における Delta の $ \eta$ が natural transformation である証明]
+                         caption= Agda における Delta の $ \eta$ が natural transformation である証明]
                         {src/delta_eta_is_nt.agda.replaced}
     \item $ \mu $ が natural transformation であること
 
@@ -253,10 +251,8 @@
 
         $ \mu $ の証明もバージョンによるパターンマッチで行なわれる。
         バージョンが1である場合は refl で証明できるが、1以上の場合に同じ証明で再帰的に定義できない。
-        なぜなら、$ \mu $ はTT に対するであり、 TT の両方のバージョンが等しい場合にのみ適用する。
-        しかし証明中で外部のTに対する演算を先に行なっているために内部の項とバージョン数が合わない項が存在する。
-        その項に対する演算を含めた等式が証明中で必須となるため、別の項に証明を分離した。
-        分離した証明 \verb/tailDelta-to-tail-nt/ では \verb/d : Delta (Delta A (S (S m))) (S n) / のように内部と外部の Nat が違うことに留意してもらいたい。
+        変形中に内部の Delta と外部の Delta のバージョン数が異なる項が存在し、バージョン数が等しい前提の $ \mu $ に適用できないためである。
+        その項に対する演算を含めた等式を別の証明 \verb/tailDelta-to-tail-nt/ として分離した。
 
 \begin{table}[html]
     \lstinputlisting[basicstyle={\scriptsize},
@@ -315,13 +311,9 @@
 
         バージョンが1である場合はやはり同じ項に簡約される。
         しかしバージョンが1以上である場合は複雑な式変形を行なう。
+        こちらでも部分的な証明\verb/delta-fmap-mu-to-tail/ を定義し、$ \mu $ が適用できない項を変形している。
 
-        パターンマッチにより最も外側の Delta は分解されるため、バージョンが1下がる。
-        しかし内側の Delta 2つはバージョンが異なるため、外側2つの Delta のバージョンが異なってしまい $ \mu $ が適用できない。
-        よって \verb/delta-fmap-mu-to-tail/ として部分的な等式を証明してから可換性を証明する。
-        \verb/delta-fmap-mu-to-tail/ では Delta のバージョンが \verb/Delta (Delta (Delta A (S (S m))) (S (S m))) (S n)/ となっていることに注目してもらいたい。
-
-        \verb/delta-fmap-mu-to-tail/ に加え、 $ \mu $ が natural transformation であることを利用して再帰的に定義することで証明ができる。
+        \verb/delta-fmap-mu-to-tail/ に加え、 $ \mu $ が natural transformation であることを利用して再帰的に定義し証明した。
 
 \end{enumerate}