Mercurial > hg > Papers > 2015 > atton-midterm
annotate bachelor_middle_draft.tex @ 4:0805d4984b1f
Update v2.1
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 29 Oct 2014 15:05:38 +0900 |
parents | 331d9984930f |
children | 156ae5d5750b |
rev | line source |
---|---|
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 \documentclass[twocolumn,twoside,9.5pt]{jarticle} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 \usepackage[dvips]{graphicx} |
2 | 3 \usepackage{cprotect} |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 \usepackage{picins} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 \usepackage{fancyhdr} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 \usepackage{eclbkbox} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 \usepackage{url} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 %\pagestyle{fancy} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 \rhead{} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 \cfoot{} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 \setlength{\headheight}{0mm} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 \setlength{\headsep}{5mm} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 \setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 \setlength{\textwidth}{181mm} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 \setlength{\textheight}{261mm} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 \setlength{\footskip}{0mm} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 \pagestyle{empty} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 \begin{document} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 \title{Modify Program by Monad} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 \author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 \date{} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 \maketitle |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 \thispagestyle{fancy} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
2 | 30 % {{{ プログラムの変更を表すMonad |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
2 | 32 \section{プログラムの変更を表すMonad} |
33 プログラムを変更するとプログラムの実行結果も変化する。 | |
34 しかし、変更後のプログラムが正しい実行結果でない場合も存在する。 | |
35 そこで、プログラムに対する変更をMonadとして記述する。 | |
3
331d9984930f
Fixes from hiyoko-san check
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
36 Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。 |
2 | 37 ひいては、プログラムを変更することの意味や性質などを解析する。 |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 % }}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 |
2 | 41 % {{{ 限定されたプログラムの変更を表す Delta Monad |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 |
2 | 43 \section{限定されたプログラムの変更を表す Delta Monad} |
3
331d9984930f
Fixes from hiyoko-san check
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
44 Monad を用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。 |
4 | 45 Haskell におけるMonadとはメタ計算を内包したデータ型である。 |
46 Monadであるデータ型は任意の型の値を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 |
2 | 48 Haskell において限定されたプログラムの変更を表すことができる Delta Monad を定義した。 |
49 Delta Monad におけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。 | |
50 また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。 | |
51 | |
52 データ型Delta の定義を示す(図\ref{delta-monad-definition})。 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 |
2 | 54 % {{{ Definiton Delta |
55 | |
56 \begin{breakbox} | |
57 \verb/ data Delta a = Delta [String] a [String] a/ | |
58 \caption{型変数を持つ型 Delta の定義(Haskell)} | |
59 \label{delta-monad-definition} | |
60 \end{breakbox} | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 % }}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 |
2 | 64 データ型 Delta は任意の型aの変数を持つことができる。 |
65 型aの変数を2つと変数に対する実行履歴となる文字列のリストを2つ持つ。 | |
66 このデータ型をMonadとして利用するが、あるデータ型をMonadとするためには関数 return と \verb/>>=/ を定義する必要がある(図\ref{monad-class})。 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 |
2 | 68 % {{{ Definiton Delta |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 \begin{breakbox} |
2 | 71 \begin{verbatim} |
72 return :: Monad m => a -> m a | |
73 (>>=) :: Monad m => m a -> (a -> m b) -> m b | |
74 \end{verbatim} | |
75 \caption{データ型をMonadとするために必要な関数} | |
76 \label{monad-class} | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 \end{breakbox} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 % }}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 |
2 | 81 図\ref{monad-class} の定義は関数の型のみ記述している。 |
82 m は Monad であり、m a は任意の型 a を内包するMonadである。 | |
83 return は任意の型aからm aの値を返す関数 return がある。 | |
84 return は任意の型の値をMonadに内包するために利用する。 | |
85 中置関数\verb/(>>=)/ はMonadの値 m a と、aを取って m b を返す関数を取り、m b の値を返す。 | |
86 \verb/(>>=)/の定義がMonadに対するメタ計算の定義となる。 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 |
2 | 88 Delta におけるreturnと\verb/>>=/の定義を図\ref{monad-instance-delta}に示す。 |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 |
2 | 90 % {{{ instance Monad Delta |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 \begin{breakbox} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 \begin{verbatim} |
2 | 94 mu (Delta lx (Delta llx x _ _) |
95 ly (Delta _ _ lly y)) = | |
96 Delta (lx ++ llx) x (ly ++ lly) y | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 |
2 | 98 instance Monad Delta where |
99 return x = Delta [] x [] x | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
100 d >>= f = mu $ fmap f d |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
101 \end{verbatim} |
2 | 102 \cprotect\caption{Delta に対する return と\verb/(>>=)/ の定義} |
103 \label{monad-instance-delta} | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
104 \end{breakbox} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
105 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
106 % }}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
107 |
2 | 108 return においては実行履歴が存在しない空の文字列を含んだMonadを返す。 |
109 型a の値xは2つに分解され、異なる実行結果を得るために利用する。 | |
110 \verb/(>>=)/においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
111 |
2 | 112 これらの関数returnと\verb/>>=/は満たすべきMonad則が存在する。 |
113 型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda\cite{agda}によって証明した。 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
114 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
115 % }}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
116 |
2 | 117 |
118 % {{{ Delta Monad におけるプログラムの変更例 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
119 |
2 | 120 \section{Delta Monad におけるプログラムの変更例} |
4 | 121 変更例となるHaskellのプログラムを示す(図\ref{raw-program-before})。 |
122 | |
123 % {{{ raw-program-before | |
124 | |
125 \begin{breakbox} | |
126 {\scriptsize | |
127 \begin{verbatim} | |
128 generator :: Int -> [Int] | |
129 generator x = [1..x] | |
130 | |
131 primeFilter :: [Int] -> [Int] | |
132 primeFilter xs = filter isPrime xs | |
133 | |
134 count :: [Int] -> Int | |
135 count xs = length xs | |
136 | |
137 primeCount :: Int -> Int | |
138 primeCount x = count . primeFilter . generator $ x | |
139 \end{verbatim} | |
140 } | |
141 \caption{変更前のHaskellプログラム} | |
142 \label{raw-program-before} | |
143 \end{breakbox} | |
144 | |
145 % }}} | |
146 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
147 |
4 | 148 このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。 |
149 1からnまでの整数の個数を調べる primeCount 関数は3つの関数からなる。 | |
150 | |
151 \begin{itemize} | |
152 \item 1 から n までの整数を返す関数 generator | |
153 \item 整数のリストから素数である整数のみを残したリストを返す関数 primeFilter | |
154 \item リストの中に存在する要素の個数を返す関数 count | |
155 \end{itemize} | |
156 | |
157 ここで、 primeFilter 関数を変更する。 | |
158 素数である整数を残すのではなく、偶数を残すようにする。 | |
159 Delta Monad を使わずに primeFilter 関数を変更すると図\ref{raw-program-after}のプログラムとなる。 | |
160 | |
161 % {{{ raw-program-after | |
162 | |
163 \begin{breakbox} | |
164 {\tt | |
165 primeFilter :: [Int] -> [Int] | |
166 | |
167 primeFilter xs = filter \underline{even} xs | |
168 } | |
169 \caption{変更後の primeFilter 関数(変更点は下線)} | |
170 \label{raw-program-after} | |
171 \end{breakbox} | |
172 | |
173 % }}} | |
174 | |
175 プログラム(図\ref{raw-program-before})に対する図\ref{raw-program-after}の変更を Delta Monad で記述したものが図\ref{delta-program}のプログラムである。 | |
176 | |
177 % {{{ delta-program | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
178 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
179 \begin{breakbox} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
180 {\scriptsize |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
181 \begin{verbatim} |
2 | 182 generator :: Int -> Delta [Int] |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
183 generator x = let intList = [1..x] in |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
184 returnD intList |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
185 |
2 | 186 primeFilter :: [Int] -> Delta [Int] |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
187 primeFilter xs = let primeList = filter isPrime xs |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
188 refactorList = filter even xs in |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
189 returnDD primeList refactorList |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
190 |
2 | 191 count :: [Int] -> Delta Int |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
192 count xs = let primeCount = length xs in |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
193 returnD primeCount |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
194 |
2 | 195 primeCount :: Int -> Delta Int |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
196 primeCount x = generator x >>= primeFilter >>= count |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
197 \end{verbatim} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
198 } |
4 | 199 \cprotect\caption{図\ref{raw-program-before}のプログラムに対する図\ref{raw-program-after}の変更を Delta Monad で記述した例} |
2 | 200 \label{delta-program} |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
201 \end{breakbox} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
202 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
203 % }}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
204 |
4 | 205 Delta Monad を用いたプログラムでは全ての関数はDelta Monadを返す関数として記述される。 |
206 変更される primeFilter 関数は、素数によるフィルタと偶数によるフィルタの両方の結果を持ったDelta Monad を返すよう変更する。 | |
2 | 207 図\ref{delta-program}のプログラムを実行した例が図\ref{delta-result}である。 |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
208 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
209 % {{{ results |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
210 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
211 \begin{breakbox} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
212 {\small |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
213 \begin{verbatim} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
214 *Main> primeCount 10 |
2 | 215 Delta |
216 ["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4 | |
217 ["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
218 \end{verbatim} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
219 } |
2 | 220 \caption{Delta Monad を用いたプログラムの実行例} |
221 \label{delta-result} | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
222 \end{breakbox} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
223 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
224 % }}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
225 |
4 | 226 Delta Monad による実行結果は2つの実行結果が存在する。 |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
227 変更前のプログラムの実行順序が上側の実行結果である。 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
228 \begin{itemize} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
229 \item 1 から 10 までのリストを作成し |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
230 \item 素数のみを残すために 2,3,5,7 が残り |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
231 \item その個数を数えるために4となる |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
232 \end{itemize} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
233 変更後のプログラムの実行順序が下側の実行結果である。 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
234 \begin{itemize} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
235 \item 1 から 10 までのリストを作成し |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
236 \item 偶数のみを残すために 2,4,6,8,10 が残り |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
237 \item その個数を数えるために5となる |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
238 \end{itemize} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
239 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
240 変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
241 この実行結果を比較することにより、変更前のプログラムの実行結果が損なわれていないか検知する。 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
242 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
243 今回は検証のために変更前と変更後の両方のプログラムを実行した。 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
244 しかし、必ず両方実行しなくてはならない訳では無い。 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
245 Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
246 そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。 |
2 | 247 遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。 |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
248 |
2 | 249 % }}} |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
250 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
251 % {{{ まとめと課題 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
252 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
253 \section{まとめと課題} |
2 | 254 Delta Monad を定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。 |
255 さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。 | |
1
9d656911de30
Comment from kono-lab-members
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
0
diff
changeset
|
256 |
2 | 257 今回定義したDelta Monad はプログラムの変更を保持できるのは1つのMonadにつき2つまでという制約がある。 |
258 Delta Monad を拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。 | |
259 Monad のみでプログラムの変更を記述することにより、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。 | |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
260 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
261 % }}} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
262 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
263 \begin{thebibliography}{9} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
264 |
2 | 265 \bibitem{moggi} Eugenio Moggi, Notion of Computation and Monads(1991) |
266 \bibitem{proofs-and-types} Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990) | |
4 | 267 \bibitem{category} Michael Barr and Chariles Wells, Category Theory for Computing Science |
2 | 268 \bibitem{agda} The Agda Wiki - Agda \url{http://wiki.portal.chalmers.se/agda/pmwiki.php} |
0
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
269 |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
270 \end{thebibliography} |
95a86a261203
Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
271 \end{document} |