--- a/prepaper/115763K.tex	Tue Feb 17 16:11:40 2015 +0900
+++ b/prepaper/115763K.tex	Tue Feb 17 16:40:06 2015 +0900
@@ -46,29 +46,24 @@
 \thispagestyle{fancy}
 
 \begin{abstract}
-We propose improvement methods to Reliability of program by formalize modification of program.
-Generally, reliability changes due to modification.
-We formalize modification of program using Monad.
-We define Delta Monad as meta computation that save program when modifies.
-Delta Monad provides functions for improve reliability.
-For example, debug method that compare traces of different versions is available.
-Finally, We proved Delta Monad satisfies Monad-laws.
+Formalization of program modification is proposed.
+Series of source code version are represented as List like structured Monad as meta compuation.
+Using this Delta Monad, we can make reliable program development possible.
+For example, comparing traces of different versions is performed in Haskell.
 \end{abstract}
 
 \section{プログラムの変更の形式化}
-信頼性とはプログラムが正しく動作する保証であり、バグといった原因により低下する。
-信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を形式化する。
-形式化には Monad を用い、メタ計算としてプログラムの変更を定義する。
-最後に、定義したメタ計算が Monad 則を満たすことを証明する。
+プログラムの変更そのものを計算に対するプログラミング、つまり、メタ計算として形式化する手法を提案する。
+メタ計算の形式化としては、Monad を使う手法がMogi~\cite{Moggi:1991:NCM:116981.116984}などにより提案されている。
+ここではプログラムの複数のバージョンを持つデータ構造Deltaを使用する。Delta がMonadであることを
+証明支援系 Agda~\cite{agdawiki}を用いて証明した。
 
-\section{メタ計算と Monad}
-プログラムを形式化するにあたり、プログラムを定義する。
-プログラムの要素は型付けされた値と関数により定義され、関数は値から値への写像を行なう。
-プログラムの実行は関数の適用として表わされる。
-この時、入出力といった値の写像で表現できない計算は Monad を用いいたメタ計算とすることで解決できる~\cite{Moggi:1991:NCM:116981.116984}。
+ここではプログラムは関数の集合であり、プログラムの変更は関数の定義の変更になる。それぞれの変更はMonadに
+格納されるために型が整合している必要がある。Delta Monad により、
+信頼性が変化する点としてのプログラムの変更を形式化することができた。
+例えば、プログラムの異なるバージョンを同時に実行し、そのトレースをMonadを用いて比較することが可能である。
 
 \section{変更を表す Delta Monad}
-プログラムの変更を表すメタ計算として、変更時に過去のプログラムも保存する Delta Monad を提案する。
 Delta Monad では変更単位をバージョンとし、全てのバージョンを保存する。
 Delta Monad をプログラミング言語 Haskell において実装し、異なるバージョンのプログラムを同時に実行する。