Mercurial > hg > Papers > 2015 > atton-midterm

comparison bachelor_middle_draft.tex @ 0:95a86a261203

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Migrate from atton/texts/bachelor_middle_draft
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 28 Oct 2014 17:28:21 +0900
parents
children 9d656911de30
comparison
equal deleted inserted replaced
-1:000000000000 0:95a86a261203
1 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
2 \usepackage[dvips]{graphicx}
3 \usepackage{picins}
4 \usepackage{fancyhdr}
5 \usepackage{eclbkbox}
6 \usepackage{url}
7 %\pagestyle{fancy}
8 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
9 \rhead{}
10 \cfoot{}
11
12 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
13 \setlength{\headheight}{0mm}
14 \setlength{\headsep}{5mm}
15 \setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
16 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
17 \setlength{\textwidth}{181mm}
18 \setlength{\textheight}{261mm}
19 \setlength{\footskip}{0mm}
20 \pagestyle{empty}
21
22 \begin{document}
23 \title{Modify Program by Monad}
24 \author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治}
25 \date{}
26 \maketitle
27 \thispagestyle{fancy}
28
29 % {{{ 研究目的
30
31 \section{研究目的と提案手法}
32 プログラムを変更するとプログラムの実行結果も変化する。
33 その際、変更前のプログラムでは正しく実行できていた内容が変更によって損なわれる場合がある。
34 プログラムの変更時に正しい実行結果が損なわれていないか自動で検知することを目的とする。
35
36 本研究では、自動で実行結果の変更を検知するために、プログラムの変更を Monad を利用して行なう。
37 Monad を利用したプログラム変更の際、変更前のプログラムを保存しながら変更する。
38 変更前のプログラムは保存されているので変更後も実行することができる。
39 両方の実行結果を比較することにより実行結果が損なわれていないか検知する。
40
41 また、プログラムの変更を Monad によって定義することによって、プログラムを変更することの意味や性質などを解析したい。
42
43 % }}}
44
45 % {{{ Monad
46
47 \section{Haskell における Monad}
48 Monad とはプログラムの型に対するメタ計算に対応するもの\cite{moggi}である。
49
50 プログラムのデータは型に所属しており、関数は型に所属する値を受けとって値を返すものとして考える。
51 その際、任意の型Aを内包する型Tを定義することができる。
52 型Aを内包した型Tを T A と記述する。
53
54 ここで、型 T A の値と型Aから型T Bに変換する関数fをとり、型 T B の値を返す関数joinを定義することができる。
55 関数join では関数f で行なわれる計算と join で行なわれる計算がある。
56 計算の区別のために後者のことをメタ計算と呼ぶ。
57 メタ計算は関数fの内容に関わらず、型Tの定義により決定する。
58 このことにより、型Tに対するjoinを定義することで型Tに対するメタ計算を定義することが可能となる。
59 型T Aの値に対し、任意の関数を適用する際にjoinを用いることで、関数適用時に型Tのメタ計算を毎回行なうことができる。
60 このように、型Tに対してメタ計算を対応させたものがMonadである。
61
62 型Aの値を型T Aの値に変更する関数と関数joinはMonad則\cite{monad-laws}(図\ref{haskell-monad-law})を満たす必要がある。
63 プログラミング言語 Haskell においては型Aの値を型T Aの値に変更する関数名は return であり、joinは中置関数 \verb/>>=/ である。
64 これらの関数2つがMonad則を満たす時、メタ計算と計算が正しく分離して行なれることが保証される。
65
66 % }}}
67
68 % {{{ Monad の定義
69
70 \section{プログラムの変更を表現するMonad}
71 プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。
72
73 % {{{ Definiton Diff
74
75 \begin{breakbox}
76 \verb/ data Diff a = Diff [String] a [String] a/
77 \caption{型変数を持つ型 Diff の定義(Haskell)}
78 \label{diff-monad-definition}
79 \end{breakbox}
80
81 % }}}
82
83 型変数aを持つデータ型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことで構成される。
84 このデータコンストラクタ Diff が型Aの変数を型 Diff A に変換するTに相当している。
85 変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。
86 文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。
87 このリストはメタ計算にのみ利用される。
88
89 次にDiffをMonadとして定義する。
90 HaskellではMonadは型に対する型クラスとして表現される。
91 型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
92 その関数群が定義された型Aを型クラスXのインスタンスであると呼ぶ。
93 ある型を型クラスMonadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。
94
95 型Diff に対して関数 return と \verb/>>=/ を定義する(図\ref{diff-monad-instance-definition})。
96 % {{{ instance Monad Diff
97
98 \begin{breakbox}
99 \begin{verbatim}
100 mu (Diff lx (Diff llx x _ _)
101 ly (Diff _ _ lly y)) =
102 Diff (lx ++ llx) x (ly ++ lly) y
103
104 instance Monad Diff where
105 return x = Diff [] x [] x
106 d >>= f = mu $ fmap f d
107 \end{verbatim}
108 \caption{Diff を Monad のインスタンスとして定義する(Haskell)}
109 \label{diff-monad-instance-definition}
110 \end{breakbox}
111
112 % }}}
113
114 return はデータコンストラクタDiffによって型Aを型Diff Aへと変換する関数である。
115 \verb/>>=/ では、メタ計算として型Diffが持っている2つ変数に対する計算を行なう。
116 片方の変数はプログラム変更前の計算を行ない、もう片方は変更後の計算を行なうようにする。
117 変更前の計算も行なうことで、変更前のプログラムの保存とする。
118
119 また、型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることは定理証明支援系プログラミング言語Agdaによって証明済みである。
120
121 % {{{ Monad-laws
122
123 \begin{breakbox}
124 \begin{verbatim}
125 return a >>= k = k a
126 m >>= return = m
127 m >>= (\x -> k x >>= h) = (m >>= k) >>= h
128 \end{verbatim}
129 \caption{Haskell における Monad則}
130 \label{haskell-monad-law}
131 \end{breakbox}
132
133 % }}}
134
135 % }}}
136
137 \section{Diff Monadを用いたプログラムの実行}
138 Diff Monad を用いたHaskellのプログラムを示す(図\ref{diff-program})。
139
140 % {{{ diff.hs
141
142 \begin{breakbox}
143 {\scriptsize
144 \begin{verbatim}
145 generator :: Int -> Diff [Int]
146 generator x = let intList = [1..x] in
147 returnD intList
148
149 primeFilter :: [Int] -> Diff [Int]
150 primeFilter xs = let primeList = filter isPrime xs
151 refactorList = filter even xs in
152 returnDD primeList refactorList
153
154 count :: [Int] -> Diff Int
155 count xs = let primeCount = length xs in
156 returnD primeCount
157
158 primeCount :: Int -> Diff Int
159 primeCount x = generator x >>= primeFilter >>= count
160 \end{verbatim}
161 }
162 \caption{Diff Monadを用いたプログラムの例}
163 \label{diff-program}
164 \end{breakbox}
165
166 % }}}
167
168 このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。
169 1からnまでの整数の個数を調べるprimeCount 関数は3つの関数からなる
170
171 \begin{itemize}
172 \item 1 から n までの整数を返す関数 generator
173 \item 整数のリストから素数であるもののみを残したリストを返す関数 primeFilter
174 \item リストの中に存在する要素の個数を返す関数 count
175 \end{itemize}
176
177 このプログラムの primeFilter 関数が返す Diff Monad を変更する。
178 本来ならば素数である整数のみを返す計算だったが、変更により偶数である整数のみを返すようにした。
179 図\ref{diff-program}のプログラムを実行した例が図\ref{diff-result}である。
180
181 % {{{ results
182
183 \begin{breakbox}
184 {\small
185 \begin{verbatim}
186 *Main> primeCount 10
187 Diff ["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4
188 ["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5
189 \end{verbatim}
190 }
191 \caption{Diff Monad を用いたプログラムの実行例}
192 \label{diff-result}
193 \end{breakbox}
194
195 % }}}
196
197 変更前のプログラムの実行順序が上側の実行結果である。
198 \begin{itemize}
199 \item 1 から 10 までのリストを作成し
200 \item 素数のみを残すために 2,3,5,7 が残り
201 \item その個数を数えるために4となる
202 \end{itemize}
203 変更後のプログラムの実行順序が下側の実行結果である。
204 \begin{itemize}
205 \item 1 から 10 までのリストを作成し
206 \item 偶数のみを残すために 2,4,6,8,10 が残り
207 \item その個数を数えるために5となる
208 \end{itemize}
209
210 変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。
211 この実行結果を比較することにより、変更前のプログラムの実行結果が損なわれていないか検知する。
212
213 今回は検証のために変更前と変更後の両方のプログラムを実行した。
214 しかし、必ず両方実行しなくてはならない訳では無い。
215 Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。
216 そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。
217 遅延評価とDiff Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
218
219
220 % {{{ まとめと課題
221
222 \section{まとめと課題}
223 Diff Monad を定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとして実行することが可能となった。
224
225 今後の課題としては大きく2つある。
226 変更の個数の拡張と Monad によってプログラムを変更することの意味を調べることである。
227 現状の Diff Monad はプログラムの変更を1つまでしか持つことができない。
228 変更を無限回行なえるDiffを定義することで、プログラムに対する変更をMonadによる変更のみで表したい。
229
230 また、プログラムに対する変更がMonadによって表される場合、圏論の視点からどのような意味が捉えられるか調査したい。
231 Monadは圏論から導入された概念であり、プログラム側のMonadと圏論側のMonadは対応している。
232 Diff Monad を圏論の観点で捉えることにより、Diff Monadの性質などを圏論側から導出できないかといった狙いがある。
233
234 ひいては、プログラムを作ることや変更することは理論的にどのような意味を持つのかを探っていきたい。
235
236 % }}}
237
238 \begin{thebibliography}{9}
239
240 \bibitem{moggi} Eugenio Moggi, Notion of Computation and Monads (1991)
241 \bibitem{monad-laws} Monad - HaskellWiki \url{http://www.haskell.org/haskellwiki/Monad}
242
243 \end{thebibliography}
244 \end{document}