\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvips]{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
\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}

\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 through 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 を用いる。
プログラムにおける Monad とはデータ構造とメタ計算の関連付けであり、メタ計算とは計算を行なう計算である。
入出力機構をプログラムの計算とは別に定義し、メタ計算とする。
メタ計算を利用したい関数は値をメタ計算と関連付けられたデータ型へと写像する。
プログラムを実行した結果のデータ型を元にメタ計算を実行することで、プログラムの内部ではメタ計算を扱うことなくメタ計算を実行できる。
これが Monad を用いた計算とメタ計算の対応である。
例えばプログラミング言語 Haskell においては、入出力処理や非決定性、失敗する可能性のある計算や例外処理などが Monad として提供されている。

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

TODO: source

バージョンが1である値はコンストラクタ Mono によって構成され、複数のバージョンを持つ場合はコンストラクタ Delta により構成される。
Delta Monad におけるプログラムは全ての値が Delta であり、全ての関数はDeltaを返す。
つまりプログラム全体においてバージョンは一意である。

TODO: temporary......


\section{他の Monad との組み合せ}

\section{まとめと課題}

\thispagestyle{fancy}
\begin{thebibliography}{9}

\bibitem{1}

\end{thebibliography}
\end{document}