# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1424143400 -32400
# Node ID 5c6f6d7b5bb5bbdd3771db22017202b392f6422f
# Parent  c75ba6313e39d21a3eaba3ac995a3a63b9d37334
Adjust prepaper

diff -r c75ba6313e39 -r 5c6f6d7b5bb5 paper/future.tex
--- a/paper/future.tex	Tue Feb 17 12:08:10 2015 +0900
+++ b/paper/future.tex	Tue Feb 17 12:23:20 2015 +0900
@@ -17,3 +17,4 @@
 category theory では category の構造から性質を導いたり、他の category への関連を導くことができる。
 プログラムの変更を Monad として表した時に持つ意味や、 category が持つ有益な性質をプログラムに適用したい。
 特に、複数のプログラムを同時に実行するのは product に、全てのプログラムを生成できる Delta 全体を表す集合は colimit に関連があると考えている。
+% TODO 本当に Delta で任意の変更を表わすことができるのか
diff -r c75ba6313e39 -r 5c6f6d7b5bb5 prepaper/115763K.tex
--- a/prepaper/115763K.tex	Tue Feb 17 12:08:10 2015 +0900
+++ b/prepaper/115763K.tex	Tue Feb 17 12:23:20 2015 +0900
@@ -59,12 +59,11 @@
 本研究はプログラムの信頼性を向上させることを目的とする。
 信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。
 信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を Monad を用いたメタ計算として形式化する。
-加えて、定義した計算が Monad 則を満たすかの証明を行なう。
+加えて、定義した計算が Monad 則を満たすか証明する。
 
 \section{メタ計算と Monad}
 プログラムを形式化するにあたり、プログラムを定義する。
-プログラムの要素は型付けされた値と関数により定義される。
-関数は値から値へ写像するものである。
+プログラムの要素は型付けされた値と関数により定義され、関数は値から値への写像を行なう。
 プログラムの実行は関数の適用として表される。
 この時、入出力といった値の写像のみで表現できない計算を表現するために Monad を用いる。
 プログラムにおける Monad とはデータ構造とメタ計算の関連付けであり、メタ計算とは計算を行なう計算である ~\cite{Moggi:1991:NCM:116981.116984}。
@@ -75,7 +74,7 @@
 本研究ではプログラムの変更を表すメタ計算として、変更時に過去のプログラムも保存するメタ計算を提案する。
 このメタ計算に対応する Monad として Delta Monad を定義し、プログラミング言語 Haskell にて実装する。
 Delta Monad では変更単位をバージョンとし、全てのバージョンを保存しつつ実行することができる。
-まずは、Delta Monad と対応するデータ型 Delta を定義する。
+まずは、Delta Monad と対応するデータ型 Delta を定義する(リスト\ref{src:delta_data})。
 
 \begin{table}[html]
     \lstinputlisting[label=src:delta_data, caption= Delta のデータ定義] {src/delta_data.hs}
@@ -85,21 +84,20 @@
 よって、最初のプログラムにおける値は Mono で構成され、値の変更を行なう時は Delta を追加することで表現する。
 そのためバージョンによって順序付けられたリストが構成される。
 
-次に Delta 型と関連付けるメタ計算を示す。
+リスト\ref{src:delta_instance_monad}に Delta 型と関連付けるメタ計算を示す。
 
 \begin{table}[html]
     \lstinputlisting[label=src:delta_instance_monad, caption= Delta に対するメタ計算の定義] {src/delta_instance_monad.hs}
 \end{table}
 
-Delta Monad では全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を実現する。
+Delta Monad は全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を行なう。
 プログラムはバージョンによって順序付けられているため、計算する際にバージョンが同じ関数と値を用いて関数を適用することで実現する。
-コンストラクタが Mono であった場合はバージョン1であるため、バージョン1どうしの計算を行なう。
-バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。
+コンストラクタが Mono であった場合はバージョン1であるためバージョン1どうしの計算を行ない、バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。
 
 \section{Delta Monad を用いたプログラムの例}
 Delta Monad を用いてプログラムの変更を記述する。
 
-まずは変更前のプログラム numberCount を示す。
+まずは変更の対象となるプログラム numberCount を示す(リスト\ref{src:numberCountV1})。
 
 \begin{table}[html]
     \lstinputlisting[label=src:numberCountV1,
@@ -127,8 +125,8 @@
 
 
 次に、numberCount プログラムを変更する。
-変更点は numberFilter 関数の抽出条件とし、素数判定による抽出から偶数判定による抽出とする。
-変更した結果をリストに示す。
+変更点は numberFilter 関数の抽出条件とし、素数判定による抽出から偶数判定による抽出に変更する。
+変更した結果をリスト\ref{src:numberCountV2}に示す。
 なお、変更部分は下線の部分である。
 
 \begin{table}[html]
@@ -155,7 +153,7 @@
     \lstinputlisting[label=src:numberCountResult, caption= Delta によって表現されたnumberCountの実行例] {src/numberCountResult.txt}
 \end{table}
 
-numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた1000が得られる。
+numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた500が得られる。
 このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行することが可能となる。
 なお、 Delta が Monadであることを保証するMonad則を満たすることは証明支援言語Agdaによって証明した。
 
@@ -163,8 +161,8 @@
 Delta Monad によりプログラムの変更を表現することができた。
 ここで Delta Monad と他の Monad の組み合せを考える。
 プログラミング言語 Haskell において、入出力は Monad を介して行なわれる。
-よって入出力を行なうプログラムでは Monad を用いるため、 Delta Monad は他の Monad と組み合せが必須となる。
-加えて、Monad により提供される例外やロギングといったメタ計算を組み合せで Delta に組込めるというメリットもある。
+よって入出力を行なうプログラムの変更を表現するには他の Monad と組み合わせが必須となる。
+加えて、Monad により提供される例外やロギングといったメタ計算を Delta に組込めるというメリットもある。
 
 Delta Monad と他の Monad を組み合せるためにデータ型 DeltaM を定義した。
 データ型 DeltaM は内部にある Monad のメタ計算と同時にDelta Monad のメタ計算を行なう。
@@ -173,7 +171,17 @@
 
 \section{まとめと課題}
 Delta Monad を用いてプログラムの変更を定義することができた。
-TODO...
+プログラムを同時に実行しながらトレースを比較することで変更を検出するなど、信頼性の向上に用いることができる。
+
+今後の課題は大きく分けて3つある。
+まず1つめはメタ計算の定義である。
+今回行なったメタ計算は変更時に前のプログラムを保存するものであった。
+他にもプログラムの変更時にトレースを確認してから変更を適用するなど、他のメタ計算が定義できると考えている。
+2つめは Delta におけるプログラムの変更範囲の定義である。
+Delta において表現可能なプログラムの変更の範囲は全ての変更を含んでいるか、もしくはどの変更が行なわれるかを定義または証明する。
+最後に Monad を通した圏における解釈がある。
+特に、バージョンの組み合せは product に、全てのバージョンを保存している Delta は colimit に対応すると考えている。
+
 
 \nocite{Girard:1989:PT:64805, opac-b1092711, BarrM:cattcs, JonesDuponcheel93}
 \thispagestyle{fancy}