\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvips]{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
\usepackage{listings}
\usepackage{url}
\pagestyle{fancy}
\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 卒業研究発表会}
\rhead{}
\cfoot{}

\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
\setlength{\headheight}{0mm}
\setlength{\headsep}{5mm}
\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
\setlength{\textwidth}{181mm}
\setlength{\textheight}{261mm}
\setlength{\footskip}{0mm}
\pagestyle{empty}


%% listings settings

\lstset{
  frame=single,
  keepspaces=true,
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  language={},
  tabsize=4,
  lineskip=-0.5zw,
  escapechar={@},
}
\def\lstlistingname{リスト}


\begin{document}
\title{Categorical Formalization of Program Modification}
\author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治}
\date{}
\maketitle
\thispagestyle{fancy}

\begin{abstract}
Reliability of program reduced by many factors.
Generally, reliability changes due to modification.
We formalize modification of program using Monad.
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.
\end{abstract}

\section{プログラムの変更の形式化}
信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。
信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を Monad を用いたメタ計算として形式化する。
加えて、定義した計算が Monad 則を満たすか証明する。

\section{メタ計算と Monad}
プログラムを形式化するにあたり、プログラムを定義する。
プログラムの要素は型付けされた値と関数により定義され、関数は値から値への写像を行なう。
プログラムの実行は関数の適用として表わされる。
この時、入出力といった値の写像で表現できない計算は Monad を用いいたメタ計算とすることで解決できる~\cite{Moggi:1991:NCM:116981.116984}。

\section{変更を表す Delta Monad}
プログラムの変更を表すメタ計算として、変更時に過去のプログラムも保存する Delta Monad を提案する。
Delta Monad では変更単位をバージョンとし、全てのバージョンを保存しつつ実行することができる。
Delta Monad をプログラミング言語 Haskell において実装し、異なるバージョンのプログラムを同時に実行する。

まずは、Delta Monad と対応するデータ型 Delta を定義する(リスト\ref{src:delta_data})。

\begin{table}[html]
    \lstinputlisting[label=src:delta_data, caption= Delta のデータ定義] {src/delta_data.hs}
\end{table}

バージョンが1である値はコンストラクタ Mono によって構成され、複数のバージョンを持つ場合はコンストラクタ Delta により構成される。
よって、最初のプログラムにおける値は Mono で構成され、値の変更を行なう時は 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 は全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を行なう。
プログラムはバージョンによって順序付けられているため、計算する際にバージョンが同じ関数と値を用いて関数を適用することで実現する。
コンストラクタが Mono であった場合はバージョン1であるためバージョン1どうしの計算を行ない、バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。

\section{Delta Monad を用いたプログラムの例}
Delta Monad を用いて、異なるバージョンのプログラムを同時に実行した例を示す。

まずは変更の対象となる numberCount プログラムのバージョン1を示す(リスト\ref{src:numberCountV1})。

\begin{table}[html]
    \lstinputlisting[label=src:numberCountV1,
                     caption= numberCount プログラムバージョン1,
                     basicstyle={\small}] {src/numberCount1.hs}
\end{table}

numberCount プログラムは、1 から n の整数において特定の数の個数を数えるプログラムである。
プログラムは3つの関数によって表現される。

{\tt generator} :
n を取り、1からnまでの整数のリストを返す

{\tt numberFilter} :
整数のリストを取り、特定の性質を持つ数のみを残す。
バージョン1では素数の数のみを残す。

{\tt count} :
整数のリストを取り、その個数を数える。

次に、numberCount プログラムを変更する。
変更点は numberFilter 関数の抽出条件とし、素数判定による抽出から偶数判定による抽出に変更する。
変更した結果をリスト\ref{src:numberCountV2}に示す。
なお、変更部分は下線の部分である。

\begin{table}[html]
    \lstinputlisting[label=src:numberCountV2,
                     caption= numberCount プログラムバージョン2,
                     basicstyle={\small}] {src/numberCount2.hs}
\end{table}

numberCount プログラムとその変更を Delta Monad によって記述する(リスト\ref{src:numberCountDelta})。
Delta Monad によって変更を記述したプログラムは全ての値が Delta 型であり、全ての関数はDelta型の値を返す。

\begin{table}[html]
    \lstinputlisting[label=src:numberCountDelta, caption= Delta を用いて記述した numberCount プログラム,
                     basicstyle={\footnotesize}] {src/numberCountDelta.hs}
\end{table}

generator 関数と count 関数は変更が無いために Mono のままである。
変更された numberFilter 関数は、返り値の Delta のバージョンを2つにしている。

Delta によって表現された numberCount プログラムを実行することで、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が得られる。
このように 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 を用いてプログラムの変更を定義することができた。
プログラムを同時に実行しながらトレースを比較することで変更を検出するなど、信頼性の向上に用いることができる。

今後の課題は大きく分けて3つある。
まず1つめはメタ計算の定義である。
今回行なったメタ計算は変更時に前のプログラムを保存するものであった。
他にもプログラムの変更時にトレースを確認してから変更を適用するなど、他のメタ計算が定義できると考えている。
2つめは Delta におけるプログラムの変更範囲の定義である。
Delta において表現可能なプログラムの変更の範囲は全ての変更を含んでいるか、もしくはどの変更が行なわれるかを定義または証明する。
最後に Monad を通した圏における解釈がある。
特に、バージョンの組み合せは product に、全てのバージョンを保存している Delta は colimit に対応すると考えている。


\nocite{Girard:1989:PT:64805, opac-b1092711, BarrM:cattcs, JonesDuponcheel93}
\thispagestyle{fancy}

\bibliographystyle{jplain}
\bibliography{reference}

\end{document}