\documentclass{ipsjpapers}

% ユーザが定義したマクロなど．
\makeatletter
\let\@ARRAY\@array \def\@array{\def\<{\inhibitglue}\@ARRAY}
\def\<{\(\langle\)\nobreak}
\def\>{\nobreak\(\rangle\)}
\def\|{\verb|}
\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\LATEX{\iLATEX\Large}
\def\LATEx{\iLATEX\normalsize}
\def\LATex{\iLATEX\small}
\def\iLATEX#1{L\kern-.36em\raise.3ex\hbox{#1\bf A}\kern-.15em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}
\def\LATEXe{\ifx\LaTeXe\undefined \LaTeX 2e\else\LaTeXe\fi}
\def\LATExe{\ifx\LaTeXe\undefined \iLATEX\scriptsize 2e\else\LaTeXe\fi}
\def\Quote{\list{}{}\item[]}
\let\endQuote\endlist
\def\TT{\if@LaTeX@e\tt\fi}
\def\CS#1{\if@LaTeX@e\tt\expandafter\string\csname#1\endcsname\else
    $\backslash$#1\fi}

%\checklines    % 行送りを確認する時に使用
\begin{document}%{
% 和文表題
\title{圏によるプログラムの変更の形式化}
% 英文表題
\etitle{Categorical Formalization of Program Modification}
% 所属ラベルの定義
\affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.}
% 和文著者名
\author{比嘉 健太\affiref{ie-ryukyu}\and
        河野 真治\affiref{ie-ryukyu}}
% 英文著者名
\eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and
        Shinji Kono\affiref{ie-ryukyu}}

% 和文概要
\begin{abstract}
本研究ではプログラムの信頼性を保ちながら開発するための手法を提案することを目的とする。

プログラムの信頼性が変化するのはプログラムの変更時である。
プログラムの変更を表現するデータ構造 Delta を定義し、異なるバージョンのプログラムを同時に実行可能にする。
異なるバージョン間のプログラムのトレースを比較し、信頼性の変化の可視化とデバッグの支援を行なう手法を提案する。

\end{abstract}
% 英文概要
\begin{eabstract}
TODO: abstract
TODO: 。とか、とか

\end{eabstract}

% 表題などの出力
\maketitle

%}{

% 本文はここから始まる
\section{はじめに}
プログラムの信頼性を保ちながら開発するための手法を提案する。
プログラムの変更時に信頼性が変化すると仮定し、圏を用いてプログラムの変更を形式化する。

本研究ではプログラムの変更を Monad として表現する。
Monad とはメタ計算と対応付けられたデータ構造である。
Monad として任意の異なるバージョンのプログラムを同時に実行するデータ構造 Delta を定義した。
プログラムの変更は特定バージョンの Delta から次のバージョンの Delta への変換として記述する。

ここで、任意の2つのバージョンのプログラムを同時に実行する。
実行した際に振舞いが変化する点がバージョン間における変更点である。
変更点を自動で検出することにより、バージョンが変わることによって信頼性の変化する部分を指摘する。

\section{プログラムの変更を表す Delta}
プログラミング言語 Haskell においてデータ構造 Delta を定義した。
Delta は全てのバージョンの実行結果の値を保持するデータ構造である。
値の変更は値から Delta を返す関数として定義する。
返す Delta に内包する値を複数個持たせることにより、複数のバージョンを表現する。

ここで、異なるバージョン数を持つ Delta や関数の組み合せを考える。
その際、前のバージョンの組み合せを保存しつつ新たな変更も取り入れるように組み合せる必要がある。
バージョンの組み合せを表現するために Delta を Monad とする。

Monad とはデータ構造とメタ計算を対応付ける手法である\cite{moggi}。
ここでのメタ計算とはバージョン間の組み合せを一意に決めるルールである。
関数の実行時にメタ計算も含めて実行することにより、異なるバージョンに存在するの独立した計算も全て実行することができる。
なお、データ構造を Monad として定義する際に満たすべき Monad則が存在するが、Monad則を満たしていることは証明支援系言語Agda\cite{agda}によって証明した。
TODO: ルールを得るサンプルを書くかな? or Delta の定義

よって、プログラムをデータ構造 Delta とDelta を返す関数として記述することにより、全てのバージョンを同時に実行できるプログラムが得られる。
ここで、バージョンとはある一意な Delta の組み合せの列として表現される。
組み合せの列を比較することにより異なるバージョン間の比較ができると考えた。


\section{任意の2つのバージョンを実行する Parallel Debugger}
任意の2つのバージョンを同時に実行することによりデバッグを支援する手法 Parallel Debugger を提案する。

Delta によって表現されたプログラムの任意のバージョンを2つ選ぶ。
2つのバージョンを同時に実行し、実行結果が変化する点を検出する。
実行結果の比較を行なうことにより、プログラムの変更時に混入したバグを発見できるのでは無いかと考えた。

さらに、2つのバージョンのうち片方を実行しつつ、もう片方はデバッグモードとして実行する。
バージョンアップ前の挙動をバージョンアップ後も保存しているか自動で確認することも可能であると考えている。
加えて、テストなどと併用することにより異なるバージョン間における信頼性や品質の比較も可能である。


\section{まとめと課題}
本研究ではプログラムの変更をMonadによって表現した。
定義したデータ構造 Delta により全てのバージョンを同時に実行できることを確認した。
Delta における特定のバージョン2つを同時に実行することにより、デバッグの支援や信頼性の比較を行なう手法 Parallel Debugger を提案した。

今後の課題としては大きく3つある。
1 つめは Delta におけるプログラムの表現能力である。
可能なプログラムの全ての変更を Delta によって表現可能かどうか調べなくてはならない。
この課題については Delta と他の Monad との組み合せが可能であれば可能であると考えている。
今回 Delta を実装した Haskell においては入出力の処理が Monad として表現される。
そのため、入出力を含めた変更は Monad との組み合せが必要になる。

2 つめはDelta におけるそれぞれのバージョンのトレースを得ることである。
異なるバージョンにおいて実行結果が変化する点を指摘するには実行結果が比較可能でなくてはいけない。
このためにバージョンごとの実行結果やトレースを得る必要がある。
この問題に対しても Monad との組み合せによって解決しようと考えている。
トレースを得る Monad を定義し、そのMonadと Delta との組み合せで各バージョンのトレースを得る。

3 つめは Delta を圏として表現することとその解析である。
Monad は Kleisli圏の Kleisli Triple との対応が存在しており\cite{category}、Deltaもある圏を構築すると考えている。
特に、 Parallel Debugger は圏における Product と対応すると考えている。
圏における他の性質から、プログラムの変更の性質の解析や他の手法を提案する。


%}{

\begin{thebibliography}{10}

\bibitem{moggi} Eugenio Moggi: Notion of Computation and Monads(1991)
\bibitem{category} Michael Barr and Charles Wells: Category Theory for Computing Science(1989)
\bibitem{proofs-and-types} Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990)
\bibitem{agda} The Agda Wiki - Agda \\ \verb|http://wiki.portal.chalmers.se/agda/pmwiki.php|

\end{thebibliography}

%}{

\end{document}