Mercurial > hg > Papers > 2015 > atton-midterm

annotate wordpress.html @ 11:ee63be7dddb4 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added tag wordpress_submit for changeset 83777243f572
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 29 Oct 2014 16:54:24 +0900
parents 83777243f572
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 <div>[toc]</div>
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 <h4>115763K:比嘉健太</h4>
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 <h4>Modify Program by Monad</h4>
10
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
4 &nbsp;
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
5 <h5>プログラムの変更を表すMonad</h5>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
6 プログラムを変更するとプログラムの実行結果も変化する。しかし、変更後のプログラムが正しい実行結果でない場合も存在する。そこで、プログラムに対する変更をMonadとして記述する。Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。ひいては、プログラムを変更することの意味や性質などを解析する。
10
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
7
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
8 &nbsp;
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
9 <h5>限定されたプログラムの変更を表すDelta Monad</h5>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
10 Monadを用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。HaskellにおけるMonadとはメタ計算を内包したデータ型である。Monadであるデータ型は任意の型の値を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
11 Haskellにおいて限定されたプログラムの変更を表すことができるDelta Monadを定義した。Delta Monadにおけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
12 データ型Deltaの定義を示す(図1)。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
13 <div title="Page 1">
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
14 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
15 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
16 <blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
17 <pre>data Delta a = Delta [String] a [String] a</pre>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
18 図 1: 型変数を持つ型 Delta の定義 (Haskell)</blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
19 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
20 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
21 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
22 データ型Deltaは任意の型aの変数を持つことができる。型aの変数を2つと変数に対する実行履歴となる文字列のリストを2つ持つ。このデータ型をMonadとして利用するが、あるデータ型をMonadとするためには関数returnと&gt;&gt;=を定義する必要がある(図2)。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
23 <div title="Page 1">
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
24 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
25 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
26 <blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
27 <pre>return :: Monad m =&gt; a -&gt; m a
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
28 (&gt;&gt;=) :: Monad m =&gt; m a -&gt; (a -&gt; m b) -&gt; m b</pre>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
29 図 2: データ型を Monad とするために必要な関数</blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
30 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
31 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
32 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
33 図2の定義は関数の型のみ記述している。mはMonadであり、m aは任意の型aを内包するMonadである。returnは任意の型aからm aの値を返す関数returnがある。returnは任意の型の値をMonadに内包するために利用する。中置関数(&gt;&gt;=)はMonadの値m aと、aを取ってm bを返す関数を取り、m bの値を返す。(&gt;&gt;=)の定義がMonadに対するメタ計算の定義となる。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
34 Deltaにおけるreturnと&gt;&gt;=の定義を図3に示す。
10
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
35 <blockquote>mu (Delta lx (Delta llx x _ _) ly (Delta _ _ lly y)) = Delta (lx ++ llx) x (ly ++ lly) y
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
37 instance Monad Delta where
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
38 return x = Delta [] x [] x
10
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
39 d &gt;&gt;= f = mu $ fmap f d
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
41 図 3: Delta に対する return と (&gt;&gt;=) の定義</blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
42 returnにおいては実行履歴が存在しない空の文字列を含んだMonadを返す。型aの値xは2つに複製され、異なる実行結果を得るために利用する。(&gt;&gt;=)においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
43 これらの関数returnと&gt;&gt;=は満たすべきMonad則が存在する。型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda[4]によって証明した。
10
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
44
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
45 &nbsp;
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
46 <h5>Delta Monadにおけるプログラムの変更例</h5>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
47 変更例となるHaskellのプログラムを示す(図4)。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
48 <blockquote>generator :: Int -&gt; [Int]
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
49 generator x = [1..x]
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
51 primeFilter :: [Int] -&gt; [Int]
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
52 primeFilter xs = filter isPrime xs
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
53
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
54 count :: [Int] -&gt; Int
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
55 count xs = length xs
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
56
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
57 primeCount :: Int -&gt; Int
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
58 primeCount x = count . primeFilter . generator $ x
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
60 図 4: 変更前の Haskell プログラム</blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
61 このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。1からnまでの整数の個数を調べるprimeCount関数は3つの関数からなる。
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 <ul>
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
63 <li>1からnまでの整数を返す関数generator</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
64 <li>整数のリストから素数である整数のみを残したリストを返す関数primeFilter</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
65 <li>リストの中に存在する要素の個数を返す関数count</li>
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 </ul>
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
67 ここで、primeFilter関数を変更する。素数である整数を残すのではなく、偶数を残すようにする。Delta Monadを使わずにprimeFilter関数を変更すると図5のプログラムとなる。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
68 <div title="Page 2">
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
69 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
70 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
71 <blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
72 <pre>primeFilter :: Int -&gt; Int
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
73 primeFilter xs = filter <span style="text-decoration: underline;"><span style="color: #000000; text-decoration: underline;">even</span></span> xs</pre>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
74 図 5: 変更後の primeFilter 関数 (変更点は下線)</blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
75 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
76 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
77 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
78 プログラム(図4)に対する図5の変更をDelta Monadで記述したものが図6のプログラムである。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
79 <blockquote>generator :: Int -&gt; Delta [Int]
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
80 generator x = let intList = [1..x] in
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
81 returnD intList
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
82
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
83 primeFilter :: [Int] -&gt; Delta [Int]
10
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
84 primeFilter xs = let primeList = <span style="text-decoration: underline;">filter isPrime xs</span>
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
85 modifiedList = <span style="text-decoration: underline;">filter even xs </span> in
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
86 returnDD primeList modifiedList
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
87
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
88 count :: [Int] -&gt; Delta Int
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
89 count xs = let primeCount = length xs in
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
90 returnD primeCount
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
92 primeCount :: Int -&gt; Delta Int
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
93 primeCount x = generator x &gt;&gt;= primeFilter &gt;&gt;= count
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
94 <div title="Page 2">
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
95 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
96 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
97 <div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
98
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
99 図 6: 図 4 のプログラムに対する図 5 の変更を Delta Monad で記述した例 (対応する変更点は下線)
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
100
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
101 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
102 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
103 </div>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
104 </div></blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
105 Delta Monadを用いたプログラムでは全ての関数はDelta Monadを返す関数として記述される。変更されるprimeFilter関数は、素数によるフィルタと偶数によるフィルタの両方の結果を持ったDelta Monadを返すよう変更する。図6のプログラムを実行した例が図7である。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
106 <blockquote>*Main&gt; primeCount 10
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
107 Delta
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
108 ["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
109 ["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
111 図 7: Delta Monad を用いたプログラムの実行例</blockquote>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
112 Delta Monadによる実行結果は2つの実行結果が存在する。変更前のプログラムの実行順序が上側の実行結果である。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
113 <ul>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
114 <li>1から10までのリストを作成し</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
115 <li>素数のみを残すために2,3,5,7が残り</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
116 <li>その個数を数えるために4となる</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
117 </ul>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
118 変更後のプログラムの実行順序が下側の実行結果である。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
119 <ul>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
120 <li>1から10までのリストを作成し</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
121 <li>偶数のみを残すために2,4,6,8,10が残り</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
122 <li>その個数を数えるために5となる</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
123 </ul>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
124 変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。この実行結果を比較することにより、プログラムがどのように変更されたか判断する。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
125 今回は検証のために変更前と変更後の両方のプログラムを実行した。しかし、必ず両方実行しなくてはならない訳では無い。Haskellには遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
10
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
126
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
127 &nbsp;
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
128 <h5>まとめと課題</h5>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
129 Delta Monadを定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
130 今回定義したDelta Monadが保持できるプログラムの変更は2つまでである。Delta Monadを拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。さらに、Monadによってプログラムの変更を記述することで、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。
10
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
131
83777243f572 Submit to wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
132 &nbsp;
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
133 <h4>別刷りPDF添付</h4>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
134 <a href="http://ie.u-ryukyu.ac.jp/dessertation/files/2014/10/115763K-midterm.pdf">115763K-midterm</a>
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 <h4>関連リンク</h4>
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 <ul>
9
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
137 <li>Eugenio Moggi, Notion of Computation and Monads(1991)</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
138 <li>Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990)</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
139 <li>Michael Barr and Charles Wells, Category Theory for Computing Science</li>
3e1c5f2f23f2 Mini updates for wordpress
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
140 <li>The Agda Wiki - Agda http://wiki.portal. chalmers.se/agda/pmwiki.php</li>
8
7f8158b0e0b5 Add html file for wordpress(manual encoding)
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 </ul>