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

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

% {{{ 研究目的

\section{研究目的と提案手法}
プログラムを変更するとプログラムの実行結果も変化する。
その際、変更前のプログラムでは正しく実行できていた内容が変更によって損なわれる場合がある。
プログラムの変更時に正しい実行結果が損なわれていないか自動で検知することを目的とする。

本研究では、自動で実行結果の変更を検知するために、プログラムの変更を Monad を利用して行なう。
Monad を利用したプログラム変更の際、変更前のプログラムを保存しながら変更する。
変更前のプログラムは保存されているため、変更後も変更前のプログラムとして実行することができる。
両方の実行結果を比較することにより実行結果が損なわれていないか検知する。

また、プログラムの変更を Monad によって定義することによって、プログラムを変更することの意味や性質などを解析する。

% }}}

% {{{ Monad

\section{Haskell における Monad}
Monad とは(TODO:どうしよう)である\cite{moggi}。
Monad の利用例としてプログラミング言語Haskellがある。
HaskellにおいてMonadはプログラムの型に対するメタ計算に対応するものである。

Haskell においてプログラムのデータは型に所属しており、関数は型に所属する値を受けとって値を返すものである。
その際、任意の型Aを内包する型Tを定義することができる。
型Aを内包した型Tを T A と記述する。

ここで、型 T A の値と型Aから型T Bに変換する関数fをとり、型 T B の値を返す関数joinを定義することができる。
関数join内では関数f の計算と join で行なわれる計算の2つがある。
計算の区別のために後者のことをメタ計算と呼ぶ。
メタ計算は関数fの内容に関わらず、型Tの定義により決定する。
このことにより、型Tに対するjoinを定義することで型Tに対するメタ計算を定義することが可能となる。
型T Aの値に対し、任意の関数を適用する際にjoinを用いることで、関数適用時に型Tのメタ計算を毎回行なうことができる。
このように、型Tに対してメタ計算を対応させたものがHaskellにおけるMonadである。

% }}}

% {{{ Monad の定義

\section{プログラムの変更を表現するMonad}
プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。

% {{{ Definiton Diff

\begin{breakbox}
\verb/ data Diff a = Diff [String] a [String] a/
\caption{型変数を持つ型 Diff の定義(Haskell)}
\label{diff-monad-definition}
\end{breakbox}

% }}}

型変数aを持つデータ型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことで構成される。
このデータコンストラクタ Diff が型Aの変数を型 Diff A に変換するTに相当している。
変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。
文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。
このリストはメタ計算にのみ利用される。

次にDiffをMonadとして定義する。
HaskellではMonadは型に対する型クラスとして表現される。
型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
その関数群が定義された型Aを型クラスXのインスタンスと呼ぶ。
ある型を型クラスMonadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。

型Diff に対して関数 return と \verb/>>=/ を定義する(図\ref{diff-monad-instance-definition})。
% {{{ instance Monad Diff

\begin{breakbox}
\begin{verbatim}
mu (Diff lx (Diff llx x _ _)
         ly (Diff _ _ lly y)) =
    Diff (lx ++ llx) x (ly ++ lly) y

instance Monad Diff where
    return x = Diff [] x [] x
    d >>= f  = mu $ fmap f d
\end{verbatim}
\caption{Diff を Monad のインスタンスとして定義する(Haskell)}
\label{diff-monad-instance-definition}
\end{breakbox}

% }}}

return はデータコンストラクタDiffによって型Aを型Diff Aへと変換する関数である。
\verb/>>=/ では、メタ計算として型Diffが持っている2つ変数に対する計算を行なう。
片方の変数はプログラム変更前の計算を行ない、もう片方は変更後の計算を行なうようにする。
変更前の計算も行なうことで、変更前のプログラムの保存とする。

なお、関数returnと \verb/>>=/ はMonad則\cite{monad-laws}(図\ref{haskell-monad-law})を満たす必要がある。
これらの関数2つがMonad則を満たす時、メタ計算と計算が正しく分離して行なれることが保証される。
型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることは定理証明支援系プログラミング言語Agdaによって証明済みである。

% {{{ Monad-laws

\begin{breakbox}
\begin{verbatim}
  return a >>= k  =  k a
  m >>= return    =  m
  m >>= (\x -> k x >>= h)  =  (m >>= k) >>= h
\end{verbatim}
\caption{Haskell における Monad則}
\label{haskell-monad-law}
\end{breakbox}

% }}}

% }}}

\section{Diff Monadを用いたプログラムの実行}
Diff Monad を用いたHaskellのプログラムを示す(図\ref{diff-program})。

% {{{ diff.hs

\begin{breakbox}
{\scriptsize
\begin{verbatim}
generator :: Int -> Diff [Int]
generator x = let intList = [1..x] in
                  returnD intList

primeFilter :: [Int] -> Diff [Int]
primeFilter xs = let primeList    = filter isPrime xs
                     refactorList = filter even xs    in
                 returnDD primeList refactorList

count :: [Int] -> Diff Int
count xs = let primeCount = length xs in
           returnD primeCount

primeCount :: Int -> Diff Int
primeCount x = generator x >>= primeFilter >>= count
\end{verbatim}
}
\caption{Diff Monadを用いたプログラムの例}
\label{diff-program}
\end{breakbox}

% }}}

このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。
1からnまでの整数の個数を調べるprimeCount 関数は3つの関数からなる

\begin{itemize}
    \item 1 から n までの整数を返す関数 generator
    \item 整数のリストから素数であるもののみを残したリストを返す関数 primeFilter
    \item リストの中に存在する要素の個数を返す関数 count
\end{itemize}

このプログラムの primeFilter 関数が返す Diff Monad を変更する。
本来ならば素数である整数のみを返す計算だったが、変更により偶数である整数のみを返すようにした。
図\ref{diff-program}のプログラムを実行した例が図\ref{diff-result}である。

% {{{ results

\begin{breakbox}
{\small
\begin{verbatim}
*Main> primeCount 10
Diff ["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4
     ["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5
\end{verbatim}
}
\caption{Diff Monad を用いたプログラムの実行例}
\label{diff-result}
\end{breakbox}

% }}}

変更前のプログラムの実行順序が上側の実行結果である。
\begin{itemize}
    \item 1 から 10 までのリストを作成し
    \item 素数のみを残すために 2,3,5,7 が残り
    \item その個数を数えるために4となる
\end{itemize}
変更後のプログラムの実行順序が下側の実行結果である。
\begin{itemize}
    \item 1 から 10 までのリストを作成し
    \item 偶数のみを残すために 2,4,6,8,10 が残り
    \item その個数を数えるために5となる
\end{itemize}

変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。
この実行結果を比較することにより、変更前のプログラムの実行結果が損なわれていないか検知する。

今回は検証のために変更前と変更後の両方のプログラムを実行した。
しかし、必ず両方実行しなくてはならない訳では無い。
Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。
そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。
遅延評価とDiff Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。


% {{{ まとめと課題

\section{まとめと課題}
Diff Monad を定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとして実行することが可能となった。

今後の課題としては大きく2つある。
変更の個数の拡張と Monad によってプログラムを変更することの意味を調べることである。

現状の Diff Monad はプログラムの変更を1つまでしか持つことができない。
変更を無限回行なえるDiffを定義することで、プログラムに対する変更をMonadによる変更のみで表現する。

また、プログラムに対する変更がMonadによって表される場合、圏論の視点からどのような意味が捉えられるか調査する。
Monadは圏論から導入された概念であり、プログラム側のMonadと圏論側のMonadは対応している。
Diff Monad を圏論の観点で捉えることにより、Diff Monadの性質などを圏論側から導出できないかといった狙いがある。

ひいては、プログラムを作ることや変更することは理論的にどのような意味を持つのかを探る。

% }}}

\begin{thebibliography}{9}

\bibitem{moggi} Eugenio Moggi, Notion of Computation and Monads (1991)
\bibitem{monad-laws} Monad - HaskellWiki \url{http://www.haskell.org/haskellwiki/Monad}

\end{thebibliography}
\end{document}