view bachelor_middle_draft/bachelor_middle_draft.tex @ 8:ffbe1bfc412c

wrote bachelor middle draft
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 26 Oct 2014 22:10:43 +0900
parents de0aa29cc3d5
children 46cf7da74731
line wrap: on
line source

\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

\section{Monad}
Monad とはプログラムのメタ計算に対応するもの\cite{moggi}である。

プログラムのデータは型に所属しており、関数は型から型への射と考える。
その際、任意の型Aを内包する型Tを定義することができる。
型Aを内包した型Tを T A と記述する。

特定の条件下において、型Aから型Bに変換する関数fを考えた時に、型 T A から型 T B に変換する関数 T f との対応が存在する。
ここで、f を T f に変換する際に特定の計算を追加することができ、T の定義時に決めることができる。
このことにより、型Aのデータに対して型Aから型Bに変換する関数fを適用するプログラムを、型T A のデータに対して型T Aから型T Bに変換する関数 T f のプログラムに変換することによって、変換前の処理に加えて型Tの定義時の計算を行なうことができる。

この特定の条件がMonad則であり、Monad則を満たす型TをMonadと呼ぶ。
Monadである型Tは変換前の計算に加えて型Tによって定義された計算を行なうことができる性質がある。
型Tによって追加される計算部分をメタ計算として定義し、プログラム全体のデータと関数を Monad によって記述することによりメタ計算を関数適用時に実行する。

% }}}

% {{{ Monad の定義

\section{プログラムの変更を表現するMonad}
プログラング言語HaskellではMonadは型に対する型クラスとして表現される。
型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
その関数群を満たした型Aを型クラスXのインスタンスであると言う。
Monadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。

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

% {{{ Definiton Diff

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

% }}}

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

型Diff を Monad のインスタンスとするために 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 のインスタンスとして定義する}
\label{diff-monad-instance-definition}
\end{breakbox}

% }}}

return はデータをMonadにするためのものであり、型aから型T aへの変換である。
\verb/>>=/ は型aから型T bに変換するための関数を用いてT aから T b への変換を定義する。
\verb/>>=/ によって計算が行なわれる際に型Diff が持っている2つ変数に対する計算を行なう。
片方はプログラム変更前の値を持ち、もう片方は変更後の値を持つようにする。

また、型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-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}