changeset 69:0cf12b73bb02

Update preprint
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 17 Feb 2015 14:50:32 +0900
parents b1271d62390c
children f44cabf175b3
files prepaper/115763K.pdf prepaper/115763K.tex
diffstat 2 files changed, 14 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
Binary file prepaper/115763K.pdf has changed
--- a/prepaper/115763K.tex	Tue Feb 17 14:32:40 2015 +0900
+++ b/prepaper/115763K.tex	Tue Feb 17 14:50:32 2015 +0900
@@ -21,7 +21,6 @@
 
 
 %% listings settings
-
 \lstset{
   frame=single,
   keepspaces=true,
@@ -53,13 +52,14 @@
 We define Delta Monad as meta computation that save behavior when modify program.
 Delta help to improve reliability.
 For example, debug method that compare traces of different versions is available.
-Finally, We proved Delta Monad satisfy Monad-laws.
+Finally, We proved Delta Monad satisfies Monad-laws.
 \end{abstract}
 
 \section{プログラムの変更の形式化}
-信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。
-信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を Monad を用いたメタ計算として形式化する。
-加えて、定義した計算が Monad 則を満たすか証明する。
+信頼性とはプログラムが正しく動作する保証であり、バグといった原因により低下する。
+信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を形式化する。
+形式化には Monad を用い、メタ計算としてプログラムの変更を定義する。
+最後に、定義したメタ計算が Monad 則を満たすか証明する。
 
 \section{メタ計算と Monad}
 プログラムを形式化するにあたり、プログラムを定義する。
@@ -88,9 +88,8 @@
     \lstinputlisting[label=src:delta_instance_monad, caption= Delta に対するメタ計算の定義] {src/delta_instance_monad.hs}
 \end{table}
 
-Delta Monad は全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を行なう。
-プログラムはバージョンによって順序付けられているため、計算する際にバージョンが同じ関数と値を用いて関数を適用することで実現する。
-コンストラクタが Mono であった場合はバージョン1であるためバージョン1どうしの計算を行ない、バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。
+プログラムはバージョンによって順序付けられているため、バージョン毎に関数を適用することでメタ計算を実現する。
+コンストラクタが Mono であるバージョン1の場合はバージョン1どうしの計算を行ない、バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。
 
 \section{Delta Monad を用いたプログラムの例}
 Delta Monad を用いて、異なるバージョンのプログラムを同時に実行した例を示す。
@@ -138,32 +137,23 @@
 generator 関数と count 関数は変更が無いために Mono のままである。
 変更された numberFilter 関数は、返り値の Delta のバージョンを2つにしている。
 
-Delta によって表現された numberCount プログラムを実行することで、2つのバージョンを同時に実行することができる。
-実行した結果がリスト\ref{src:numberCountResult}である。
+Delta によってプログラムの変更が表現できるため、2つのバージョンを含むプログラムを作成できた。
+このプログラムは全てのバージョンを同時に実行することが可能であり、実行した結果がリスト\ref{src:numberCountResult}である。
 
 \begin{table}[html]
     \lstinputlisting[label=src:numberCountResult, caption= Delta によって表現されたnumberCountの実行例] {src/numberCountResult.txt}
 \end{table}
 
-numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた500が得られる。
+numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた500が得られた。
 このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行することが可能となる。
 なお、 Delta が Monadであることを保証するMonad則を満することを証明支援言語Agda~\cite{agdawiki}によって証明した。
 
-\section{他の Monad との組み合せ}
-Delta Monad によりプログラムの変更を表現することができた。
-ここで Delta Monad と他の Monad の組み合せを考える。
-プログラミング言語 Haskell において、入出力は Monad を介して行なわれる。
-よって入出力を行なうプログラムの変更を表現するには他の Monad と組み合わせが必須となる。
-加えて、Monad により提供される例外やロギングといったメタ計算を Delta に組込めるというメリットもある。
-
-Delta Monad と他の Monad を組み合せるためにデータ型 DeltaM を定義した。
-データ型 DeltaM は内部にある Monad のメタ計算と同時にDelta Monad のメタ計算を行なう。
-例えば、DeltaM と Writer Monad を組み合せることにより、実行中の値のログ付きで全バージョン実行を行なうことができる。
-DeltaM も Monad 則を満たすことは Agda によって証明した。
-
 \section{まとめと課題}
 Delta Monad を用いてプログラムの変更を定義することができた。
-プログラムを同時に実行しながらトレースを比較することで変更を検出するなど、信頼性の向上に用いることができる。
+Delta Monad は他の Monad とも合成することが可能であり、データ型 DeltaM を定義することで Haskell における Monad 間の合成を確認できた。
+実行時のトレースや例外を表現する Monad と組み合せることで、プログラムの変更に対する解析が可能となる。
+例えば、プログラムを同時に実行しながらトレースを比較することでデバッグを支援することができる。
+他にも、全ての変更を保存する性質から、プログラムのバージョン管理システムに対して形式的な定義を与えられる。
 
 今後の課題は大きく分けて3つある。
 まず1つめはメタ計算の定義である。