Mercurial > hg > Members > atton > texts

comparison bachelor_middle_draft/bachelor_middle_draft.tex @ 9:46cf7da74731

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update bachelor middle draft
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 26 Oct 2014 23:38:29 +0900
parents ffbe1bfc412c
children
comparison
equal deleted inserted replaced
8:ffbe1bfc412c 9:46cf7da74731
26 \maketitle 26 \maketitle
27 \thispagestyle{fancy} 27 \thispagestyle{fancy}
28 28
29 % {{{ 研究目的 29 % {{{ 研究目的
30 30
31 \section{研究目的} 31 \section{研究目的と提案手法}
32 プログラムを変更するとプログラムの実行内容も変更される。 32 プログラムを変更するとプログラムの実行結果も変化する。
33 その際、変更前のプログラムでは正しく実行できていた内容が変更によって損なわれる場合がある。 33 その際、変更前のプログラムでは正しく実行できていた内容が変更によって損なわれる場合がある。
34 プログラムの変更を Monad によって行なうことにより、変更前のプログラムも保存しながらプログラムを変更する。 34 プログラムの変更時に正しい実行結果が損なわれていないか自動で検知することを目的とする。
35 35
36 さらに、プログラムの変更を Monad によって定義することにより、プログラムを変更することの意味や性質などを解析する。 36 本研究では、自動で実行結果の変更を検知するために、プログラムの変更を Monad を利用して行なう。
37 Monad を利用したプログラム変更の際、変更前のプログラムを保存しながら変更する。
38 変更前のプログラムは保存されているので変更後も実行することができる。
39 両方の実行結果を比較することにより実行結果が損なわれていないか検知する。
40
41 また、プログラムの変更を Monad によって定義することによって、プログラムを変更することの意味や性質などを解析したい。
37 42
38 % }}} 43 % }}}
39 44
40 % {{{ Monad 45 % {{{ Monad
41 46
42 \section{Monad} 47 \section{Haskell における Monad}
43 Monad とはプログラムのメタ計算に対応するもの\cite{moggi}である。 48 Monad とはプログラムの型に対するメタ計算に対応するもの\cite{moggi}である。
44 49
45 プログラムのデータは型に所属しており、関数は型から型への射と考える。 50 プログラムのデータは型に所属しており、関数は型に所属する値を受けとって値を返すものとして考える。
46 その際、任意の型Aを内包する型Tを定義することができる。 51 その際、任意の型Aを内包する型Tを定義することができる。
47 型Aを内包した型Tを T A と記述する。 52 型Aを内包した型Tを T A と記述する。
48 53
49 特定の条件下において、型Aから型Bに変換する関数fを考えた時に、型 T A から型 T B に変換する関数 T f との対応が存在する。 54 ここで、型 T A の値と型Aから型T Bに変換する関数fをとり、型 T B の値を返す関数joinを定義することができる。
50 ここで、f を T f に変換する際に特定の計算を追加することができ、T の定義時に決めることができる。 55 関数join では関数f で行なわれる計算と join で行なわれる計算がある。
51 このことにより、型Aのデータに対して型Aから型Bに変換する関数fを適用するプログラムを、型T A のデータに対して型T Aから型T Bに変換する関数 T f のプログラムに変換することによって、変換前の処理に加えて型Tの定義時の計算を行なうことができる。 56 計算の区別のために後者のことをメタ計算と呼ぶ。
52 57 メタ計算は関数fの内容に関わらず、型Tの定義により決定する。
53 この特定の条件がMonad則であり、Monad則を満たす型TをMonadと呼ぶ。 58 このことにより、型Tに対するjoinを定義することで型Tに対するメタ計算を定義することが可能となる。
54 Monadである型Tは変換前の計算に加えて型Tによって定義された計算を行なうことができる性質がある。 59 型T Aの値に対し、任意の関数を適用する際にjoinを用いることで、関数適用時に型Tのメタ計算を毎回行なうことができる。
55 型Tによって追加される計算部分をメタ計算として定義し、プログラム全体のデータと関数を Monad によって記述することによりメタ計算を関数適用時に実行する。 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則を満たす時、メタ計算と計算が正しく分離して行なれることが保証される。
56 65
57 % }}} 66 % }}}
58 67
59 % {{{ Monad の定義 68 % {{{ Monad の定義
60 69
61 \section{プログラムの変更を表現するMonad} 70 \section{プログラムの変更を表現するMonad}
62 プログラング言語HaskellではMonadは型に対する型クラスとして表現される。
63 型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
64 その関数群を満たした型Aを型クラスXのインスタンスであると言う。
65 Monadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。
66
67 プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。 71 プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。
68 72
69 % {{{ Definiton Diff 73 % {{{ Definiton Diff
70 74
71 \begin{breakbox} 75 \begin{breakbox}
72 \verb/ data Diff a = Diff [String] a [String] a/ 76 \verb/ data Diff a = Diff [String] a [String] a/
73 \caption{型変数を持つ型 Diff の定義} 77 \caption{型変数を持つ型 Diff の定義(Haskell)}
74 \label{diff-monad-definition} 78 \label{diff-monad-definition}
75 \end{breakbox} 79 \end{breakbox}
76 80
77 % }}} 81 % }}}
78 82
79 型変数aを持つ data 型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことによって構成される。 83 型変数aを持つデータ型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことで構成される。
80 このデータコンストラクタ Diff が型aの変数を型 Diff a に変換するTに相当している。 84 このデータコンストラクタ Diff が型Aの変数を型 Diff A に変換するTに相当している。
81 変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。 85 変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。
82 文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。 86 文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。
83 計算そのものに対しては影響しない。 87 このリストはメタ計算にのみ利用される。
84 88
85 型Diff を Monad のインスタンスとするために return と \verb/>>=/ を定義する(図\ref{diff-monad-instance-definition})。 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})。
86 % {{{ instance Monad Diff 96 % {{{ instance Monad Diff
87 97
88 \begin{breakbox} 98 \begin{breakbox}
89 \begin{verbatim} 99 \begin{verbatim}
90 mu (Diff lx (Diff llx x _ _) 100 mu (Diff lx (Diff llx x _ _)
93 103
94 instance Monad Diff where 104 instance Monad Diff where
95 return x = Diff [] x [] x 105 return x = Diff [] x [] x
96 d >>= f = mu $ fmap f d 106 d >>= f = mu $ fmap f d
97 \end{verbatim} 107 \end{verbatim}
98 \caption{Diff を Monad のインスタンスとして定義する} 108 \caption{Diff を Monad のインスタンスとして定義する(Haskell)}
99 \label{diff-monad-instance-definition} 109 \label{diff-monad-instance-definition}
100 \end{breakbox} 110 \end{breakbox}
101 111
102 % }}} 112 % }}}
103 113
104 return はデータをMonadにするためのものであり、型aから型T aへの変換である。 114 return はデータコンストラクタDiffによって型Aを型Diff Aへと変換する関数である。
105 \verb/>>=/ は型aから型T bに変換するための関数を用いてT aから T b への変換を定義する。 115 \verb/>>=/ では、メタ計算として型Diffが持っている2つ変数に対する計算を行なう。
106 \verb/>>=/ によって計算が行なわれる際に型Diff が持っている2つ変数に対する計算を行なう。 116 片方の変数はプログラム変更前の計算を行ない、もう片方は変更後の計算を行なうようにする。
107 片方はプログラム変更前の値を持ち、もう片方は変更後の値を持つようにする。 117 変更前の計算も行なうことで、変更前のプログラムの保存とする。
108 118
109 また、型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることをAgdaによって証明した。 119 また、型Diffが Monad則(図\ref{haskell-monad-law})を満たしていることは定理証明支援系プログラミング言語Agdaによって証明済みである。
110 120
111 % {{{ Monad-laws 121 % {{{ Monad-laws
112 122
113 \begin{breakbox} 123 \begin{breakbox}
114 \begin{verbatim} 124 \begin{verbatim}
164 \item リストの中に存在する要素の個数を返す関数 count 174 \item リストの中に存在する要素の個数を返す関数 count
165 \end{itemize} 175 \end{itemize}
166 176
167 このプログラムの primeFilter 関数が返す Diff Monad を変更する。 177 このプログラムの primeFilter 関数が返す Diff Monad を変更する。
168 本来ならば素数である整数のみを返す計算だったが、変更により偶数である整数のみを返すようにした。 178 本来ならば素数である整数のみを返す計算だったが、変更により偶数である整数のみを返すようにした。
169 変更後のプログラムを実行した例が図\ref{diff-result}である。 179 図\ref{diff-program}のプログラムを実行した例が図\ref{diff-result}である。
170 180
171 % {{{ results 181 % {{{ results
172 182
173 \begin{breakbox} 183 \begin{breakbox}
174 {\small 184 {\small
195 \item 1 から 10 までのリストを作成し 205 \item 1 から 10 までのリストを作成し
196 \item 偶数のみを残すために 2,4,6,8,10 が残り 206 \item 偶数のみを残すために 2,4,6,8,10 が残り
197 \item その個数を数えるために5となる 207 \item その個数を数えるために5となる
198 \end{itemize} 208 \end{itemize}
199 209
200 変更前の実行結果を保存しながらプログラムを変更し、新しい実行結果が得られた。 210 変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。
201 今回は検証のために両方の実行順を評価した。 211 この実行結果を比較することにより、変更前のプログラムの実行結果が損なわれていないか検知する。
202 しかし Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。 212
203 よって、変更後のプログラムのみを計算する場合は変更前の計算は行なわれない。 213 今回は検証のために変更前と変更後の両方のプログラムを実行した。
214 しかし、必ず両方実行しなくてはならない訳では無い。
215 Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。
216 そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。
204 遅延評価とDiff Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。 217 遅延評価とDiff Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
205 218
206 219
207 % {{{ まとめと課題 220 % {{{ まとめと課題
208 221