Mercurial > hg > Papers > 2015 > atton-thesis

comparison prepaper/115763K.tex @ 63:c75ba6313e39

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing prepaper...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 17 Feb 2015 12:08:10 +0900
parents 36795f6b6e87
children 5c6f6d7b5bb5
comparison
equal deleted inserted replaced
62:36795f6b6e87 63:c75ba6313e39
1 \documentclass[twocolumn,twoside,9.5pt]{jarticle} 1 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
2 \usepackage[dvips]{graphicx} 2 \usepackage[dvips]{graphicx}
3 \usepackage{picins} 3 \usepackage{picins}
4 \usepackage{fancyhdr} 4 \usepackage{fancyhdr}
5 \usepackage{listings}
5 \pagestyle{fancy} 6 \pagestyle{fancy}
6 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 卒業研究発表会} 7 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 卒業研究発表会}
7 \rhead{} 8 \rhead{}
8 \cfoot{} 9 \cfoot{}
9 10
14 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}} 15 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
15 \setlength{\textwidth}{181mm} 16 \setlength{\textwidth}{181mm}
16 \setlength{\textheight}{261mm} 17 \setlength{\textheight}{261mm}
17 \setlength{\footskip}{0mm} 18 \setlength{\footskip}{0mm}
18 \pagestyle{empty} 19 \pagestyle{empty}
20
21
22 %% listings settings
23
24 \lstset{
25 frame=single,
26 keepspaces=true,
27 basicstyle={\ttfamily},
28 breaklines=true,
29 xleftmargin=0zw,
30 xrightmargin=0zw,
31 framerule=.2pt,
32 columns=[l]{fullflexible},
33 language={},
34 tabsize=4,
35 lineskip=-0.5zw,
36 escapechar={@},
37 }
38 \def\lstlistingname{リスト}
39
19 40
20 \begin{document} 41 \begin{document}
21 \title{Categorical Formalization of Program Modification} 42 \title{Categorical Formalization of Program Modification}
22 \author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治} 43 \author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治}
23 \date{} 44 \date{}
33 For example, debug method that compare traces of different versions is available. 54 For example, debug method that compare traces of different versions is available.
34 Finally, We proved Delta Monad satisfy Monad-laws. 55 Finally, We proved Delta Monad satisfy Monad-laws.
35 \end{abstract} 56 \end{abstract}
36 57
37 \section{プログラムの変更の形式化} 58 \section{プログラムの変更の形式化}
38 本研究ではプログラムの信頼性を向上させることを目的とする。 59 本研究はプログラムの信頼性を向上させることを目的とする。
39 信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。 60 信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。
40 信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を形式化する。 61 信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を Monad を用いたメタ計算として形式化する。
41 特に本研究では Monad を用いたメタ計算としてプログラムの変更を記述する。
42 加えて、定義した計算が Monad 則を満たすかの証明を行なう。 62 加えて、定義した計算が Monad 則を満たすかの証明を行なう。
43 63
44 \section{メタ計算と Monad} 64 \section{メタ計算と Monad}
45 プログラムを形式化するにあたり、プログラムを定義する。 65 プログラムを形式化するにあたり、プログラムを定義する。
46 プログラムの要素は型付けされた値と関数により定義される。 66 プログラムの要素は型付けされた値と関数により定義される。
47 関数は値から値へ写像するものである。 67 関数は値から値へ写像するものである。
48 プログラムの実行は関数の適用として表される。 68 プログラムの実行は関数の適用として表される。
49 この時、入出力といった値の写像のみで表現できない計算を表現するために Monad を用いる。 69 この時、入出力といった値の写像のみで表現できない計算を表現するために Monad を用いる。
50 プログラムにおける Monad とはデータ構造とメタ計算の関連付けであり、メタ計算とは計算を行なう計算である。 70 プログラムにおける Monad とはデータ構造とメタ計算の関連付けであり、メタ計算とは計算を行なう計算である ~\cite{Moggi:1991:NCM:116981.116984}。
51 入出力機構をプログラムの計算とは別に定義し、メタ計算とする。 71 メタ計算として入出力機構をプログラムの計算とは別に定義し、入出力を利用したい関数は値をメタ計算と関連付けられたデータ型へと写像することで実現する。
52 メタ計算を利用したい関数は値をメタ計算と関連付けられたデータ型へと写像する。 72 Monad を用いることでプログラムの内部ではメタ計算を扱わずにメタ計算を実現できる。
53 プログラムを実行した結果のデータ型を元にメタ計算を実行することで、プログラムの内部ではメタ計算を扱うことなくメタ計算を実行できる。
54 これが Monad を用いた計算とメタ計算の対応である。
55 例えばプログラミング言語 Haskell においては、入出力処理や非決定性、失敗する可能性のある計算や例外処理などが Monad として提供されている。
56 73
57 \section{変更を表す Delta Monad} 74 \section{変更を表す Delta Monad}
58 本研究ではプログラムの変更を表すメタ計算として、変更の時に過去のプログラムも保存するメタ計算を提案する。 75 本研究ではプログラムの変更を表すメタ計算として、変更時に過去のプログラムも保存するメタ計算を提案する。
59 このメタ計算に対応する Monad として Delta Monad をプログラミング言語 Haskell にて実装する。 76 このメタ計算に対応する Monad として Delta Monad を定義し、プログラミング言語 Haskell にて実装する。
60 Delta Monad では変更単位をバージョンとし、全てのバージョンを保存しつつ実行することができる。 77 Delta Monad では変更単位をバージョンとし、全てのバージョンを保存しつつ実行することができる。
61 Delta Monad と対応するデータ型Delta を定義する。 78 まずは、Delta Monad と対応するデータ型 Delta を定義する。
62 79
63 TODO: source 80 \begin{table}[html]
81 \lstinputlisting[label=src:delta_data, caption= Delta のデータ定義] {src/delta_data.hs}
82 \end{table}
64 83
65 バージョンが1である値はコンストラクタ Mono によって構成され、複数のバージョンを持つ場合はコンストラクタ Delta により構成される。 84 バージョンが1である値はコンストラクタ Mono によって構成され、複数のバージョンを持つ場合はコンストラクタ Delta により構成される。
66 Delta Monad におけるプログラムは全ての値が Delta であり、全ての関数はDeltaを返す。 85 よって、最初のプログラムにおける値は Mono で構成され、値の変更を行なう時は Delta を追加することで表現する。
67 つまりプログラム全体においてバージョンは一意である。 86 そのためバージョンによって順序付けられたリストが構成される。
68 87
69 TODO: temporary...... 88 次に Delta 型と関連付けるメタ計算を示す。
89
90 \begin{table}[html]
91 \lstinputlisting[label=src:delta_instance_monad, caption= Delta に対するメタ計算の定義] {src/delta_instance_monad.hs}
92 \end{table}
93
94 Delta Monad では全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を実現する。
95 プログラムはバージョンによって順序付けられているため、計算する際にバージョンが同じ関数と値を用いて関数を適用することで実現する。
96 コンストラクタが Mono であった場合はバージョン1であるため、バージョン1どうしの計算を行なう。
97 バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。
98
99 \section{Delta Monad を用いたプログラムの例}
100 Delta Monad を用いてプログラムの変更を記述する。
101
102 まずは変更前のプログラム numberCount を示す。
103
104 \begin{table}[html]
105 \lstinputlisting[label=src:numberCountV1,
106 caption= numberCount プログラムバージョン1,
107 basicstyle={\small}] {src/numberCount1.hs}
108 \end{table}
109
110 numberCount プログラムは、1 から n の整数において特定の数の個数を数えるプログラムである。
111 プログラムは3つの関数によって表現される。
112 \begin{itemize}
113 \item generator
114
115 n を取り、1からnまでの整数のリストを返す
116
117 \item numberFilter
118
119 整数のリストを取り、特定の性質を持つ数のみを残す。
120 バージョン1では素数の数のみを残す。
121
122 \item count
123
124 整数のリストを取り、その個数を数える。
125
126 \end{itemize}
70 127
71 128
129 次に、numberCount プログラムを変更する。
130 変更点は numberFilter 関数の抽出条件とし、素数判定による抽出から偶数判定による抽出とする。
131 変更した結果をリストに示す。
132 なお、変更部分は下線の部分である。
133
134 \begin{table}[html]
135 \lstinputlisting[label=src:numberCountV2,
136 caption= numberCount プログラムバージョン2,
137 basicstyle={\small}] {src/numberCount2.hs}
138 \end{table}
139
140 numberCount プログラムとその変更を Delta Monad によって記述する(リスト\ref{src:numberCountDelta})。
141 Delta Monad によって変更を記述したプログラムは全ての値が Delta 型であり、全ての関数はDelta型の値を返す。
142
143 \begin{table}[html]
144 \lstinputlisting[label=src:numberCountDelta, caption= Delta を用いて記述した numberCount プログラム,
145 basicstyle={\footnotesize}] {src/numberCountDelta.hs}
146 \end{table}
147
148 generator 関数と count 関数は変更が無いために Mono のままである。
149 変更された numberFilter 関数は、返り値の Delta のバージョンを2つにしている。
150
151 Delta によって表現された numberCount プログラムを実行することで、2つのバージョンを同時に実行することができる。
152 実行した結果がリスト\ref{src:numberCountResult}である。
153
154 \begin{table}[html]
155 \lstinputlisting[label=src:numberCountResult, caption= Delta によって表現されたnumberCountの実行例] {src/numberCountResult.txt}
156 \end{table}
157
158 numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた1000が得られる。
159 このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行することが可能となる。
160 なお、 Delta が Monadであることを保証するMonad則を満たすることは証明支援言語Agdaによって証明した。
161
72 \section{他の Monad との組み合せ} 162 \section{他の Monad との組み合せ}
163 Delta Monad によりプログラムの変更を表現することができた。
164 ここで Delta Monad と他の Monad の組み合せを考える。
165 プログラミング言語 Haskell において、入出力は Monad を介して行なわれる。
166 よって入出力を行なうプログラムでは Monad を用いるため、 Delta Monad は他の Monad と組み合せが必須となる。
167 加えて、Monad により提供される例外やロギングといったメタ計算を組み合せで Delta に組込めるというメリットもある。
168
169 Delta Monad と他の Monad を組み合せるためにデータ型 DeltaM を定義した。
170 データ型 DeltaM は内部にある Monad のメタ計算と同時にDelta Monad のメタ計算を行なう。
171 例えば、DeltaM と Writer Monad を組み合せることにより、実行中の値のログ付きで全バージョン実行を行なうことができる。
172 DeltaM も Monad 則を満たすことは Agda によって証明した。
73 173
74 \section{まとめと課題} 174 \section{まとめと課題}
175 Delta Monad を用いてプログラムの変更を定義することができた。
176 TODO...
75 177
178 \nocite{Girard:1989:PT:64805, opac-b1092711, BarrM:cattcs, JonesDuponcheel93}
76 \thispagestyle{fancy} 179 \thispagestyle{fancy}
77 \begin{thebibliography}{9}
78 180
79 \bibitem{1} 181 \bibliographystyle{jplain}
182 \bibliography{reference}
80 183
81 \end{thebibliography}
82 \end{document} 184 \end{document}