Mercurial > hg > Papers > 2015 > atton-midterm

comparison bachelor_middle_draft.tex @ 2:514bb884084c

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