--- a/.hgignore	Tue Oct 28 18:23:36 2014 +0900
+++ b/.hgignore	Wed Oct 29 09:11:46 2014 +0900
@@ -7,3 +7,4 @@
 *.aux
 *.dvi
 *.toc
+*.cpt

Binary file bachelor_middle_draft.pdf has changed

--- a/bachelor_middle_draft.tex	Tue Oct 28 18:23:36 2014 +0900
+++ b/bachelor_middle_draft.tex	Wed Oct 29 09:11:46 2014 +0900
@@ -1,5 +1,6 @@
 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
 \usepackage[dvips]{graphicx}
+\usepackage{cprotect}
 \usepackage{picins}
 \usepackage{fancyhdr}
 \usepackage{eclbkbox}
@@ -26,141 +27,124 @@
 \maketitle
 \thispagestyle{fancy}
 
-% {{{ 研究目的
-
-\section{研究目的と提案手法}
-プログラムを変更するとプログラムの実行結果も変化する。
-その際、変更前のプログラムでは正しく実行できていた内容が変更によって損なわれる場合がある。
-プログラムの変更時に正しい実行結果が損なわれていないか自動で検知することを目的とする。
+% {{{ プログラムの変更を表すMonad
 
-本研究では、自動で実行結果の変更を検知するために、プログラムの変更を Monad を利用して行なう。
-Monad を利用したプログラム変更の際、変更前のプログラムを保存しながら変更する。
-変更前のプログラムは保存されているため、変更後も変更前のプログラムとして実行することができる。
-両方の実行結果を比較することにより実行結果が損なわれていないか検知する。
-
-また、プログラムの変更を Monad によって定義することによって、プログラムを変更することの意味や性質などを解析する。
+\section{プログラムの変更を表すMonad}
+プログラムを変更するとプログラムの実行結果も変化する。
+しかし、変更後のプログラムが正しい実行結果でない場合も存在する。
+そこで、プログラムに対する変更をMonadとして記述する。
+Monadとして記述した変更により、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。
+ひいては、プログラムを変更することの意味や性質などを解析する。
 
 % }}}
 
-% {{{ Monad
+% {{{ 限定されたプログラムの変更を表す Delta Monad
 
-\section{Haskell における Monad}
-Monad とは(TODO:どうしよう)である\cite{moggi}。
-Monad の利用例としてプログラミング言語Haskellがある。
-HaskellにおいてMonadはプログラムの型に対するメタ計算に対応するものである。
+\section{限定されたプログラムの変更を表す Delta Monad}
+Monad を用いてプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。
+Haskell におけるMonadとはメタ計算と対応されたデータ型である。
+Monadは任意の型を内包することができるデータ型である。
+内包した型に対する演算を行なった際、Monadに対して定義されたメタ計算も行なう。
 
-Haskell においてプログラムのデータは型に所属しており、関数は型に所属する値を受けとって値を返すものである。
-その際、任意の型Aを内包する型Tを定義することができる。
-型Aを内包した型Tを T A と記述する。
+Haskell において限定されたプログラムの変更を表すことができる Delta Monad を定義した。
+Delta Monad におけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。
+また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。
+
+データ型Delta の定義を示す(図\ref{delta-monad-definition})。
 
-ここで、型 T A の値と型Aから型T Bに変換する関数fをとり、型 T B の値を返す関数joinを定義することができる。
-関数join内では関数f の計算と join で行なわれる計算の2つがある。
-計算の区別のために後者のことをメタ計算と呼ぶ。
-メタ計算は関数fの内容に関わらず、型Tの定義により決定する。
-このことにより、型Tに対するjoinを定義することで型Tに対するメタ計算を定義することが可能となる。
-型T Aの値に対し、任意の関数を適用する際にjoinを用いることで、関数適用時に型Tのメタ計算を毎回行なうことができる。
-このように、型Tに対してメタ計算を対応させたものがHaskellにおけるMonadである。
+% {{{ Definiton Delta
+
+\begin{breakbox}
+\verb/ data Delta a = Delta [String] a [String] a/
+\caption{型変数を持つ型 Delta の定義(Haskell)}
+\label{delta-monad-definition}
+\end{breakbox}
 
 % }}}
 
-% {{{ Monad の定義
+データ型 Delta は任意の型aの変数を持つことができる。
+型aの変数を2つと変数に対する実行履歴となる文字列のリストを2つ持つ。
+このデータ型をMonadとして利用するが、あるデータ型をMonadとするためには関数 return と \verb/>>=/ を定義する必要がある(図\ref{monad-class})。
 
-\section{プログラムの変更を表現するMonad}
-プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。
-
-% {{{ Definiton Diff
+% {{{ Definiton Delta
 
 \begin{breakbox}
-\verb/ data Diff a = Diff [String] a [String] a/
-\caption{型変数を持つ型 Diff の定義(Haskell)}
-\label{diff-monad-definition}
+\begin{verbatim}
+  return :: Monad m => a -> m a
+  (>>=) :: Monad m => m a -> (a -> m b) -> m b
+\end{verbatim}
+\caption{データ型をMonadとするために必要な関数}
+\label{monad-class}
 \end{breakbox}
 
 % }}}
 
-型変数aを持つデータ型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことで構成される。
-このデータコンストラクタ Diff が型Aの変数を型 Diff A に変換するTに相当している。
-変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。
-文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。
-このリストはメタ計算にのみ利用される。
+図\ref{monad-class} の定義は関数の型のみ記述している。
+m は Monad であり、m a は任意の型 a を内包するMonadである。
+return は任意の型aからm aの値を返す関数 return がある。
+return は任意の型の値をMonadに内包するために利用する。
+中置関数\verb/(>>=)/ はMonadの値 m a と、aを取って m b を返す関数を取り、m b の値を返す。
+\verb/(>>=)/の定義がMonadに対するメタ計算の定義となる。
 
-次にDiffをMonadとして定義する。
-HaskellではMonadは型に対する型クラスとして表現される。
-型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
-その関数群が定義された型Aを型クラスXのインスタンスと呼ぶ。
-ある型を型クラスMonadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。
+Delta におけるreturnと\verb/>>=/の定義を図\ref{monad-instance-delta}に示す。
 
-型Diff に対して関数 return と \verb/>>=/ を定義する(図\ref{diff-monad-instance-definition})。
-% {{{ instance Monad Diff
+% {{{ instance Monad Delta
 
 \begin{breakbox}
 \begin{verbatim}
-mu (Diff lx (Diff llx x _ _)
-         ly (Diff _ _ lly y)) =
-    Diff (lx ++ llx) x (ly ++ lly) y
+mu (Delta lx (Delta llx x _ _)
+          ly (Delta _ _ lly y)) =
+    Delta (lx ++ llx) x (ly ++ lly) y
 
-instance Monad Diff where
-    return x = Diff [] x [] x
+instance Monad Delta where
+    return x = Delta [] x [] x
     d >>= f  = mu $ fmap f d
 \end{verbatim}
-\caption{Diff を Monad のインスタンスとして定義する(Haskell)}
-\label{diff-monad-instance-definition}
+\cprotect\caption{Delta に対する return と\verb/(>>=)/ の定義}
+\label{monad-instance-delta}
 \end{breakbox}
 
 % }}}
 
-return はデータコンストラクタDiffによって型Aを型Diff Aへと変換する関数である。
-\verb/>>=/ では、メタ計算として型Diffが持っている2つ変数に対する計算を行なう。
-片方の変数はプログラム変更前の計算を行ない、もう片方は変更後の計算を行なうようにする。
-変更前の計算も行なうことで、変更前のプログラムの保存とする。
-
-なお、関数returnと \verb/>>=/ はMonad則\cite{monad-laws}(図\ref{haskell-monad-law})を満たす必要がある。
-これらの関数2つがMonad則を満たす時、メタ計算と計算が正しく分離して行なれることが保証される。
-型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることは定理証明支援系プログラミング言語Agdaによって証明済みである。
+return においては実行履歴が存在しない空の文字列を含んだMonadを返す。
+型a の値xは2つに分解され、異なる実行結果を得るために利用する。
+\verb/(>>=)/においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。
 
-% {{{ Monad-laws
-
-\begin{breakbox}
-\begin{verbatim}
-  return a >>= k  =  k a
-  m >>= return    =  m
-  m >>= (\x -> k x >>= h)  =  (m >>= k) >>= h
-\end{verbatim}
-\caption{Haskell における Monad則}
-\label{haskell-monad-law}
-\end{breakbox}
+これらの関数returnと\verb/>>=/は満たすべきMonad則が存在する。
+型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda\cite{agda}によって証明した。
 
 % }}}
 
-% }}}
+
+% {{{ Delta Monad におけるプログラムの変更例
 
-\section{Diff Monadを用いたプログラムの実行}
-Diff Monad を用いたHaskellのプログラムを示す(図\ref{diff-program})。
+\section{Delta Monad におけるプログラムの変更例}
+Delta Monad を用いたHaskellのプログラムを示す(図\ref{delta-program})。
 
-% {{{ diff.hs
+% {{{ delta.hs
 
 \begin{breakbox}
 {\scriptsize
 \begin{verbatim}
-generator :: Int -> Diff [Int]
+generator :: Int -> Delta [Int]
 generator x = let intList = [1..x] in
                   returnD intList
 
-primeFilter :: [Int] -> Diff [Int]
+primeFilter :: [Int] -> Delta [Int]
 primeFilter xs = let primeList    = filter isPrime xs
                      refactorList = filter even xs    in
                  returnDD primeList refactorList
 
-count :: [Int] -> Diff Int
+count :: [Int] -> Delta Int
 count xs = let primeCount = length xs in
            returnD primeCount
 
-primeCount :: Int -> Diff Int
+primeCount :: Int -> Delta Int
 primeCount x = generator x >>= primeFilter >>= count
 \end{verbatim}
 }
-\caption{Diff Monadを用いたプログラムの例}
-\label{diff-program}
+\caption{Delta Monadを用いたプログラムの例}
+\label{delta-program}
 \end{breakbox}
 
 % }}}
@@ -174,9 +158,9 @@
     \item リストの中に存在する要素の個数を返す関数 count
 \end{itemize}
 
-このプログラムの primeFilter 関数が返す Diff Monad を変更する。
+このプログラムの primeFilter 関数が返す Delta Monad を変更する。
 本来ならば素数である整数のみを返す計算だったが、変更により偶数である整数のみを返すようにした。
-図\ref{diff-program}のプログラムを実行した例が図\ref{diff-result}である。
+図\ref{delta-program}のプログラムを実行した例が図\ref{delta-result}である。
 
 % {{{ results
 
@@ -184,12 +168,13 @@
 {\small
 \begin{verbatim}
 *Main> primeCount 10
-Diff ["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4
-     ["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5
+Delta
+  ["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4
+  ["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5
 \end{verbatim}
 }
-\caption{Diff Monad を用いたプログラムの実行例}
-\label{diff-result}
+\caption{Delta Monad を用いたプログラムの実行例}
+\label{delta-result}
 \end{breakbox}
 
 % }}}
@@ -214,32 +199,27 @@
 しかし、必ず両方実行しなくてはならない訳では無い。
 Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。
 そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。
-遅延評価とDiff Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
+遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
 
+% }}}
 
 % {{{ まとめと課題
 
 \section{まとめと課題}
-Diff Monad を定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとして実行することが可能となった。
-
-今後の課題としては大きく2つある。
-変更の個数の拡張と Monad によってプログラムを変更することの意味を調べることである。
+Delta Monad を定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。
+さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。
 
-現状の Diff Monad はプログラムの変更を1つまでしか持つことができない。
-変更を無限回行なえるDiffを定義することで、プログラムに対する変更をMonadによる変更のみで表現する。
-
-また、プログラムに対する変更がMonadによって表される場合、圏論の視点からどのような意味が捉えられるか調査する。
-Monadは圏論から導入された概念であり、プログラム側のMonadと圏論側のMonadは対応している。
-Diff Monad を圏論の観点で捉えることにより、Diff Monadの性質などを圏論側から導出できないかといった狙いがある。
-
-ひいては、プログラムを作ることや変更することは理論的にどのような意味を持つのかを探る。
+今回定義したDelta Monad はプログラムの変更を保持できるのは1つのMonadにつき2つまでという制約がある。
+Delta Monad を拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。
+Monad のみでプログラムの変更を記述することにより、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。
 
 % }}}
 
 \begin{thebibliography}{9}
 
-\bibitem{moggi} Eugenio Moggi, Notion of Computation and Monads (1991)
-\bibitem{monad-laws} Monad - HaskellWiki \url{http://www.haskell.org/haskellwiki/Monad}
+\bibitem{moggi} Eugenio Moggi, Notion of Computation and Monads(1991)
+\bibitem{proofs-and-types} Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990)
+\bibitem{agda} The Agda Wiki - Agda \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}
 
 \end{thebibliography}
 \end{document}