Mercurial > hg > Papers > 2015 > atton-thesis

comparison delta.tex @ 57:5f0e13923cfd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 16 Feb 2015 16:24:42 +0900
parents 37a832dff044
children
comparison
equal deleted inserted replaced
56:398b42a1ac19 57:5f0e13923cfd
8 % {{{ Delta Monad の定義 8 % {{{ Delta Monad の定義
9 9
10 \section{Delta Monad の定義} 10 \section{Delta Monad の定義}
11 11
12 まずはプログラムを定義する。 12 まずはプログラムを定義する。
13 プログラムは型付けされた値と、値を値へと写像する関数のみで構成されるものとする。 13 プログラムは型付けされた値と、値を値へと写像する関数のみで構成される。
14 プログラムの実行は関数の値への適用とする。 14 プログラムの実行は関数の値への適用とする。
15 入出力といった、値や関数で表現できない計算はメタ計算とする。 15 入出力といった、値や関数のみで表現できない計算はメタ計算とする。
16 メタ計算をある性質を持つデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。 16 メタ計算を特定のデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。
17 メタ計算とデータ構造の対応に用いる性質が Monad である。 17 メタ計算とデータ構造の対応に用いる性質が Monad である。
18 18
19 例えば、失敗する可能性があるメタ計算 T は式\ref{exp:partiality}のように定義できる。 19 例えば、失敗する可能性があるメタ計算 T は式\ref{exp:partiality}のように定義できる。
20 20
21 \begin{equation} 21 \begin{equation}
22 T A = A_{ \bot } (i.e. A + \left\{ \bot \right\}) 22 T A = A_{ \bot } (i.e. A + \left\{ \bot \right\})
23 \label{exp:partiality} 23 \label{exp:partiality}
24 \end{equation} 24 \end{equation}
25 25
26 型 A の値に対応するメタ計算 T は、A と $ \bot $ の論理和として表現できる。 26 型 A の値に対応するメタ計算 T は、A と $ \bot $ の論理和として表現できる。
27 成功した際は A を返し、失敗した場合は $ \bot $ を返す。 27 計算に成功した際は A を返し、失敗した場合は $ \bot $ を返す。
28 28
29 ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させるとする。 29 ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させる。
30 プログラムは型付けされた値と、関数の組み合せで構成される。 30 プログラムは型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。
31 例えば、型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。
32 31
33 \begin{equation} 32 \begin{equation}
34 g ( f ( x )) 33 g ( f ( x ))
35 \label{exp:non_failure_program} 34 \label{exp:non_failure_program}
36 \end{equation} 35 \end{equation}
37 36
38 ここで関数f は失敗する可能性があるとする。 37 ここで関数f は失敗する可能性があるとする。
39 その時、f が失敗した場合の計算を考える必要がある。 38 その時、f が失敗した場合の計算を考える必要がある。
40 計算の実現方法はいくつか存在する。 39 この計算の実現方法はいくつか存在する。
41 計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で行なうことで実現できる。 40 計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で判断するなどがある。
42 41
43 実現方法の1つとして、 Monad を用いたメタ計算がある。 42 実現方法の1つとして、 Monad を用いたメタ計算がある。
44 Monad により失敗した際の計算をメタ計算としてデータ構造に紐付ける。 43 Monad により失敗した際の計算をメタ計算としてデータ構造に紐付ける。
45 式\ref{exp:partiality} で定義したように、計算の成功は型 A 値を返し、失敗は $ \bot $ を返す。 44 式\ref{exp:partiality} で定義したように、計算の成功は型 A 値を返し、失敗は $ \bot $ を返す。
46 計算に失敗した際に対応するメタ計算を定義し、関数をそのメタ計算で拡張することで失敗に対する処理が実現できる。 45 計算に失敗した際に対応するメタ計算を定義し、関数をそのメタ計算で拡張することで失敗に対する処理が実現できる。
47 例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することが実現できる。 46 例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することができる。
48 47
49 型A を持つx の値をメタ計算と対応して型 T A とした値を x' 、メタ計算による関数の拡張を * と記述すると、式\ref{exp:non_failure_program} の式は式\ref{exp:failure_program} のように書ける。 48 型A を持つx の値をメタ計算と対応して型 T A とした値を x' 、メタ計算による関数の拡張を * と記述すると、式\ref{exp:non_failure_program} の式は式\ref{exp:failure_program} のように書ける。
50 49
51 \begin{equation} 50 \begin{equation}
52 g^{*} ( f^{*} ( x' )) 51 g^{*} ( f^{*} ( x' ))
55 54
56 ここで重要な点は、元の関数 $ f $ と $g$ から $f^{*}$ と $g^{*}$ が導けることである。 55 ここで重要な点は、元の関数 $ f $ と $g$ から $f^{*}$ と $g^{*}$ が導けることである。
57 メタ計算が無い関数 $ f $ とメタ計算を持つ関数 $ f^{*} $ が1対1に対応することは Monad により保証されている。 56 メタ計算が無い関数 $ f $ とメタ計算を持つ関数 $ f^{*} $ が1対1に対応することは Monad により保証されている。
58 このように、値と関数で表されたプログラムにおいてメタ計算を用いることで、計算を拡張することができる。 57 このように、値と関数で表されたプログラムにおいてメタ計算を用いることで、計算を拡張することができる。
59 58
60 プログラムの変更をメタ計算として記述することを考える。 59 プログラムとメタ計算の関係としての Monad について述べたところで、プログラムの変更をメタ計算として記述することを考える。
61 60
62 ここで、プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。 61 プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。
63 最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。 62 最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。
64 任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義する。 63 任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義する。
65 64
66 \begin{equation} 65 \begin{equation}
67 T A = V A 66 T A = V_A
68 \label{exp:meta_computation_definition} 67 \label{exp:meta_computation_definition}
69 \end{equation} 68 \end{equation}
70 69
71 V はプログラムの全てバージョンの集合であり、V AとすることでAに対応する値の集合を返すものとする。 70 V はプログラムの全てバージョンの集合であり、$ V_A $ とすることでAに対応する値の集合を返すものとする。
72 71
73 ここで、プログラムが変更される際に過去のバージョンのプログラムも保存するメタ計算を提案する。 72 式\ref{exp:meta_computation_definition}のメタ計算として、全ての変更単位で変更されたプログラムを保存する計算を提案する。
74 全ての変更単位で変更されたプログラムを保存し、それらを比較することでプログラムの変更を表現しようと考えた。 73 このメタ計算を Delta Monad と呼ぶ。
75 このメタ計算を表す Monad を Delta Monad と呼ぶ。
76 なお、この Delta Monadが Monad であることの証明は \ref{chapter:proof_delta} 章で行なう 74 なお、この Delta Monadが Monad であることの証明は \ref{chapter:proof_delta} 章で行なう
77 75
78 % }}} 76 % }}}
79 77
80 % {{{ Haskell における Delta Monad の実装例 78 % {{{ Haskell における Delta Monad の実装例
114 なお、関数型は \verb/ a -> b / のように引数の型と返り値の型を \verb/->/で挟んで記述する。 112 なお、関数型は \verb/ a -> b / のように引数の型と返り値の型を \verb/->/で挟んで記述する。
115 引数が2つ以上の関数は \verb/ a -> b -> ... -> d / のように \verb/->/を増やすことで記述する。 113 引数が2つ以上の関数は \verb/ a -> b -> ... -> d / のように \verb/->/を増やすことで記述する。
116 114
117 関数 return は任意の型aを受けとり、メタ計算と対応された型に対応させて返す。 115 関数 return は任意の型aを受けとり、メタ計算と対応された型に対応させて返す。
118 \verb/>>=/ は中置関数であり、left operand と right operand を取る。 116 \verb/>>=/ は中置関数であり、left operand と right operand を取る。
119 left operand であるメタ計算と対応された値と、right operand であるメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。 117 left operand にメタ計算と対応された値と、right operand にメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。
120 118
121 データ型 Delta に対応するメタ計算を Monad を用いてリスト\ref{src:delta_instance_monad}のように定義する。 119 データ型 Delta に対応するメタ計算を Monad を用いてリスト\ref{src:delta_instance_monad}のように定義する。
122 120
123 \begin{table}[html] 121 \begin{table}[html]
124 \lstinputlisting[label=src:delta_instance_monad, caption=Haskell におけるデータ型Deltaとメタ計算の関連付け] 122 \lstinputlisting[label=src:delta_instance_monad, caption=Haskell におけるデータ型Deltaとメタ計算の関連付け]
131 通常の値をメタ計算と対応させるため、値をバージョン1の値とする。 129 通常の値をメタ計算と対応させるため、値をバージョン1の値とする。
132 そのためにコンストラクタ Mono を用いる。 130 そのためにコンストラクタ Mono を用いる。
133 131
134 \item 中置関数 \verb/>>=/ 132 \item 中置関数 \verb/>>=/
135 133
136 メタ計算を含んだ関数の適用であるため、値と関数の同じバージョンを計算して返すものとなる。 134 メタ計算を含んだ関数の適用である。
135 通常の関数の適用に加え、バージョンを含んだ計算も行なう。
136 値と関数のそれぞれにおいて同じバージョン選択し、関数を適用する。
137 もしバージョン1であった場合はコンストラクタは Mono であるため、Mono が持っている値に対して関数を適用することとなる。 137 もしバージョン1であった場合はコンストラクタは Mono であるため、Mono が持っている値に対して関数を適用することとなる。
138 もしバージョンが1で無い場合のコンストラクタは Delta であるため、先頭の値を用いて計算し、残りの値と結合することとなる。 138 もしバージョンが1で無い場合のコンストラクタは Delta であるため、先頭の値を用いて計算し、残りの値と結合することとなる。
139 その際、先頭の値を取り出すために headDelta 関数を、先頭以外の値を取り出すために tailDelta 関数を用いる。 139 その際、先頭の値を取り出すために headDelta 関数を、先頭以外の値を取り出すために tailDelta 関数を用いる。
140 \end{itemize} 140 \end{itemize}
141 141
192 つまり、Monad によってプログラムの変更をメタ計算として定義できたと言える。 192 つまり、Monad によってプログラムの変更をメタ計算として定義できたと言える。
193 193
194 Haskell において実装した Delta Monad はプログラムの変更を含めた計算もメタ計算としてHaskellで実行する。 194 Haskell において実装した Delta Monad はプログラムの変更を含めた計算もメタ計算としてHaskellで実行する。
195 これはプログラムの変更からどのような処理を導くかをメタ計算として Haskell で実行可能であることを意味する。 195 これはプログラムの変更からどのような処理を導くかをメタ計算として Haskell で実行可能であることを意味する。
196 つまり、図\ref{fig:non_delta_example}のようにプログラムにおいてバージョンが変わるごとにバージョン間の関係が存在しない状態から、図\ref{fig:delta_example}のようにプログラムの変更を含めてプログラムを実行可能となったことを意味する。 196 つまり、図\ref{fig:non_delta_example}のようにプログラムにおいてバージョンが変わるごとにバージョン間の関係が存在しない状態から、図\ref{fig:delta_example}のようにプログラムの変更を含めてプログラムを実行可能となったことを意味する。
197 例えば、プログラムの実行時にバージョン間の挙動の比較することで過去の挙動との差異を指摘することなどが可能となる。 197 メタ計算を変更することでプログラムの実行時にバージョン間の挙動の比較することも可能となる。
198 198
199 \begin{figure}[htbp] 199 \begin{figure}[htbp]
200 \begin{center} 200 \begin{center}
201 \includegraphics[scale=0.8]{fig/non_delta_example.pdf} 201 \includegraphics[scale=0.8]{fig/non_delta_example.pdf}
202 \caption{Deltaを用いない通常のプログラムの例} 202 \caption{Deltaを用いない通常のプログラムの例}
221 \ref{section:delta_example}節ではプログラムの変更に対して、変更前と変更後の挙動を保存した例を述べた。 221 \ref{section:delta_example}節ではプログラムの変更に対して、変更前と変更後の挙動を保存した例を述べた。
222 \ref{section:delta_merit}節ではプログラムの変更に対するメタ計算の例を述べる。 222 \ref{section:delta_merit}節ではプログラムの変更に対するメタ計算の例を述べる。
223 223
224 まず最初に挙げられるものがプログラムの変更を保存するメタ計算である。 224 まず最初に挙げられるものがプログラムの変更を保存するメタ計算である。
225 これは Delta Monad として実際に定義できた。 225 これは Delta Monad として実際に定義できた。
226 プログラムの変更を保存した場合、以下のような方法により信頼性の向上が見込めると考える。 226 プログラムの変更を保存した場合、以下のような計算可能となる。
227 227
228 \begin{itemize} 228 \begin{itemize}
229 229
230 \item 異なるバージョンを同時に実行する 230 \item 異なるバージョンを同時に実行する
231 231
232 プログラムの変更列から任意のバージョン2つを取り出し、同時に実行するプログラムを構成する。 232 プログラムの変更列から任意のバージョン2つを取り出し、同時に実行するプログラムを構成する。
233 プログラムを同時に実行することで以下のようなメリットがある。 233 プログラムを同時に実行することで以下のようなメリットがある。
234 なお、任意の要素の組み合せは category において product として表現されるため、 product と対応があると考えている。 234 なお、任意の要素どうしの組み合せは category において product として表現されるため、 product と対応があると考えている。
235 235
236 \begin{itemize} 236 \begin{itemize}
237 \item 実行系とサブの実行系を実行することができる。 237 \item 実行系とサブの実行系を実行する
238 238
239 例えば、あるバージョンでリリースしたプログラムがあるとする。 239 例えば、あるバージョンでリリースしたプログラムがあるとする。
240 変更を加え、ベータ版としてリリースしたいが動作が不安定である。 240 変更を加え、ベータ版としてリリースしたいが動作が不安定である。
241 そこで、リリースしたプログラムからベータ版への変更から、2つのプログラムが同時に動くようなプログラムを構築する。 241 そこで、リリースしたプログラムからベータ版への変更から、2つのプログラムが同時に動くようなプログラムを構築する。
242 見掛け上は安定版として動作するが、安定版の実際の入出力を用いてベータ版をテストすることが可能となる。 242 見掛け上は安定版として動作するが、安定版の実際の入出力を用いてベータ版をテストすることが可能となる。
243 243
244 \item バージョン依存のプロトコル間で互換を持つようなプログラムが作成できる 244 \item バージョン依存のプロトコル間で互換を持つようなプログラムが作成できる
245 245
246 異なるバージョン間でプロトコルに互換が無いプログラムを考える。 246 異なるバージョン間でプロトコルに互換が無いプログラムを考える。
247 バージョン間の互換を含めてメタ計算として定義し、全てのバージョンに対して互換を持つプログラムを構築する。 247 バージョン間の互換を含めてメタ計算として定義し、全てのバージョンに対して互換を持つプログラムを構築する。
248 そうすることによりどのバージョンのプロトコルとも互換を持つような変換器を作成できる。 248 そうすることで、どのバージョンのプロトコルとも互換を持つような変換器を作成できる。
249 249
250 \end{itemize} 250 \end{itemize}
251 251
252 \item バージョン間の動作の比較 252 \item バージョン間の動作の比較
253 253
256 トレースの比較により以下のようなものを検出できると考えている。 256 トレースの比較により以下のようなものを検出できると考えている。
257 257
258 \begin{itemize} 258 \begin{itemize}
259 \item 過去のバージョンの挙動を破壊する時を検出する 259 \item 過去のバージョンの挙動を破壊する時を検出する
260 260
261 プログラムの変更の際、トレースを変えてはいけない部分が存在するとする。 261 プログラムの変更の際、トレースを変えてはいけない部分を指定する。
262 変更の際にトレースが変更したことを検出することにより、トレースが保存される変更のみを受けつけるようにする。 262 変更の際にトレースが保存される変更のみを受けつけるようにする。
263 263
264 \item トレースが変化していないことを確認する 264 \item トレースが変化していないことを確認する
265 265
266 プログラムの変更にはいくつかの種類がある。 266 プログラムの変更にはいくつかの種類がある。
267 例えば機能拡張の変更などであればトレースは変化するのが正しい。 267 例えば機能拡張の変更などであればトレースは変化するのが正しい。
282 例えばプログラムの変更単位に対してテストを行なうことで、変更に応じてテストの結果の変動が確認できる。 282 例えばプログラムの変更単位に対してテストを行なうことで、変更に応じてテストの結果の変動が確認できる。
283 プログラム全体に対応するテストを定義し、変更の際にテストが通る変更のみ受け付けるようにすることでテストベースの信頼性を確保できる。 283 プログラム全体に対応するテストを定義し、変更の際にテストが通る変更のみ受け付けるようにすることでテストベースの信頼性を確保できる。
284 \end{itemize} 284 \end{itemize}
285 285
286 他にもプログラムの変更そのものを処理するプログラムを定義することもできる。 286 他にもプログラムの変更そのものを処理するプログラムを定義することもできる。
287 この機構を言語処理系に組込むことにより、プログラムの変更方法も言語の仕様に含めることができる。 287 この機構を言語処理系に組込むことにより、言語の仕様にプログラムの変更方法も含めることができる。
288 例えば、プログラムの変更は許可されたオペレーション内で行なうといった制約を含めることが可能となる。 288 例えば、プログラムの変更は許可されたオペレーション内で行なうといった制約を加えることが可能となる。
289 さらにユーザによりプログラムの変更に対するメタ計算を自由に定義できるような言語処理系を作るとする。 289 さらにユーザによりプログラムの変更に対するメタ計算を自由に定義できるような言語処理系を作るとする。
290 その処理系ではこれまでに挙げた全てのメタ計算の例から使いたい機能を選んだり自分で追加することが可能となる。 290 その処理系ではこれまでに挙げた全てのメタ計算の例から使いたい機能を選んだり自分で追加することが可能となる。
291 291
292 このように、プログラムの変更を形式化することで多くのメタ計算が扱えるようになる。 292 このように、プログラムの変更を形式化することで多くのメタ計算が扱えるようになる。
293 さらに、メタ計算の内容によっては信頼性の向上に用いたり変更も含めた上でプログラムを作成することが可能になる。 293 さらに、メタ計算の内容によっては信頼性の向上に用いたり変更も含めた上でプログラムを作成することが可能になる。