changeset 73:f090afc484e2 prepaper_submit

Update prepaper
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 17 Feb 2015 16:50:11 +0900
parents 109c5bc7e276
children 3bfbf78cf502
files prepaper/115763K.pdf prepaper/115763K.tex
diffstat 2 files changed, 18 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
Binary file prepaper/115763K.pdf has changed
--- a/prepaper/115763K.tex	Tue Feb 17 16:40:06 2015 +0900
+++ b/prepaper/115763K.tex	Tue Feb 17 16:50:11 2015 +0900
@@ -47,20 +47,20 @@
 
 \begin{abstract}
 Formalization of program modification is proposed.
-Series of source code version are represented as List like structured Monad as meta compuation.
+Series of source code version are represented as List like structured Monad as meta computation.
 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 を使う手法がMogi~\cite{Moggi:1991:NCM:116981.116984}などにより提案されている。
-ここではプログラムの複数のバージョンを持つデータ構造Deltaを使用する。Delta がMonadであることを
-証明支援系 Agda~\cite{agdawiki}を用いて証明した。
+メタ計算の形式化としては、Monad を使う手法がMoggi~\cite{Moggi:1991:NCM:116981.116984}などにより提案されている。
+ここではプログラムの複数のバージョンを持つデータ構造Deltaを使用する。
+Delta がMonadであることを証明支援系 Agda~\cite{agdawiki}を用いて証明した。
 
-ここではプログラムは関数の集合であり、プログラムの変更は関数の定義の変更になる。それぞれの変更はMonadに
-格納されるために型が整合している必要がある。Delta Monad により、
-信頼性が変化する点としてのプログラムの変更を形式化することができた。
+ここではプログラムは関数の集合であり、プログラムの変更は関数の定義の変更となる。
+それぞれの変更はMonadに格納されるために型が整合している必要がある。
+Delta Monad により、信頼性が変化する点としてのプログラムの変更を形式化することができた。
 例えば、プログラムの異なるバージョンを同時に実行し、そのトレースをMonadを用いて比較することが可能である。
 
 \section{変更を表す Delta Monad}
@@ -74,7 +74,6 @@
 \end{table}
 
 バージョンが1である値はコンストラクタ Mono によって構成し、複数のバージョンを持つ場合はコンストラクタ Delta により構成する。
-よって、最初のプログラムにおける値は Mono で、値の変更は Delta を追加することで表現する。
 このようにプログラムの変更を記述することで、バージョンによって順序付けられたリストが構成される。
 
 リスト\ref{src:delta_instance_monad}に Delta 型と関連付けるメタ計算を示す。
@@ -87,7 +86,7 @@
 コンストラクタが Mono であるバージョン1の場合はバージョン1どうしの計算を行ない、バージョンが1より大きい Delta である場合は、再帰的にバージョンを下げながら計算を行なう。
 
 \section{Delta Monad を用いたプログラムの例}
-Delta Monad を用いて、異なるバージョンのプログラムを同時に実行した例を示す。
+Delta Monad を用いて、異なるバージョンのプログラムを同時に実行する例を示す。
 
 まずは変更の対象となる numberCount プログラムのバージョン1を示す(リスト\ref{src:numberCountV1})。
 
@@ -132,7 +131,7 @@
 generator 関数と count 関数は変更が無いために Mono のままである。
 変更された numberFilter 関数は、返り値の Delta のバージョンを2つにしている。
 
-Delta によってプログラムの変更が表現できるため、2つのバージョンを含むプログラムを作成できた。
+Delta によってプログラムの変更を表現し、2つのバージョンを含むプログラムを作成できた。
 このプログラムは全てのバージョンを同時に実行することが可能であり、実行した結果がリスト\ref{src:numberCountResult}である。
 
 \begin{table}[html]
@@ -140,23 +139,22 @@
 \end{table}
 
 numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた500が得られた。
-このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行することが可能となる。
-なお、 Delta が Monadであることを保証するMonad則を満することを証明支援言語Agda~\cite{agdawiki}によって証明した。
+このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行可能となる。
 
 \section{まとめと課題}
-Delta Monad を用いてプログラムの変更を定義することができた。
-Delta Monad は他の Monad とも合成することが可能であり、データ型 DeltaM を定義することで Haskell における Monad 間の合成を確認できた。
+Delta Monad を用いてプログラムの変更を定義し、異なるバージョンのプログラムを同時に実行することができた。
+
+また、Delta Monad は他の Monad とも合成が可能であることも証明した。
 実行時のトレースや例外を表現する Monad と組み合せることで、プログラムの変更に対する解析が可能となる。
-例えば、プログラムを同時に実行しながらトレースを比較することでデバッグを支援することができる。
-他にも、全ての変更を保存する性質から、プログラムのバージョン管理システムに対して形式的な定義を与えられる。
+Monad と合成することにより、プログラムを同時に実行しながらトレースを比較することが可能となり、デバッグを支援できる。
+なお、 Haskell においてデータ型 DeltaM を定義することで Monad を合成し、トレースを得ながら異なるバージョンのプログラムを同時に実行することができた。
 
-今後の課題は大きく分けて2つある。
-1つめは Delta Monad におけるプログラムの変更範囲の定義である。
+今後の課題は Delta Monad におけるプログラムの変更範囲の定義である。
 Delta Monad において表現可能な変更の範囲が全ての変更を含むか証明する。
 もしくは、Delta Monad により表現できる変更の範囲を定義する。
-次に Monad を通した圏における解釈がある。
+次に、 Monad を通した圏における解釈がある。
 バージョンの組み合せは product に、全てのバージョンを保存している Delta は colimit に対応すると考えている。
-
+また、全ての変更を保存する性質から、プログラムのバージョン管理システムに対して形式的な定義を与えられると考えている。
 
 \nocite{Girard:1989:PT:64805, opac-b1092711, BarrM:cattcs, JonesDuponcheel93}
 \thispagestyle{fancy}