Mercurial > hg > Papers > 2015 > atton-midterm

comparison wordpress.html @ 10:83777243f572 wordpress_submit

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Submit to wordpress
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 29 Oct 2014 16:54:18 +0900
parents 3e1c5f2f23f2
children
comparison
equal deleted inserted replaced
9:3e1c5f2f23f2 10:83777243f572
1 <div>[toc]</div> 1 <div>[toc]</div>
2 <h4>115763K:比嘉健太</h4> 2 <h4>115763K:比嘉健太</h4>
3 <h4>Modify Program by Monad</h4> 3 <h4>Modify Program by Monad</h4>
4 &nbsp;
4 <h5>プログラムの変更を表すMonad</h5> 5 <h5>プログラムの変更を表すMonad</h5>
5 プログラムを変更するとプログラムの実行結果も変化する。しかし、変更後のプログラムが正しい実行結果でない場合も存在する。そこで、プログラムに対する変更をMonadとして記述する。Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。ひいては、プログラムを変更することの意味や性質などを解析する。 6 プログラムを変更するとプログラムの実行結果も変化する。しかし、変更後のプログラムが正しい実行結果でない場合も存在する。そこで、プログラムに対する変更をMonadとして記述する。Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。ひいては、プログラムを変更することの意味や性質などを解析する。
7
8 &nbsp;
6 <h5>限定されたプログラムの変更を表すDelta Monad</h5> 9 <h5>限定されたプログラムの変更を表すDelta Monad</h5>
7 Monadを用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。HaskellにおけるMonadとはメタ計算を内包したデータ型である。Monadであるデータ型は任意の型の値を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。 10 Monadを用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。HaskellにおけるMonadとはメタ計算を内包したデータ型である。Monadであるデータ型は任意の型の値を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。
8 Haskellにおいて限定されたプログラムの変更を表すことができるDelta Monadを定義した。Delta Monadにおけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。 11 Haskellにおいて限定されたプログラムの変更を表すことができるDelta Monadを定義した。Delta Monadにおけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。
9 データ型Deltaの定義を示す(図1)。 12 データ型Deltaの定義を示す(図1)。
10 <div title="Page 1"> 13 <div title="Page 1">
27 </div> 30 </div>
28 </div> 31 </div>
29 </div> 32 </div>
30 図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に対するメタ計算の定義となる。 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に対するメタ計算の定義となる。
31 Deltaにおけるreturnと&gt;&gt;=の定義を図3に示す。 34 Deltaにおけるreturnと&gt;&gt;=の定義を図3に示す。
32 <blockquote>mu (Delta lx (Delta llx x _ _) 35 <blockquote>mu (Delta lx (Delta llx x _ _) ly (Delta _ _ lly y)) = Delta (lx ++ llx) x (ly ++ lly) y
33 ly (Delta _ _ lly y)) =
34 Delta (lx ++ llx) x (ly ++ lly) y
35 36
36 instance Monad Delta where 37 instance Monad Delta where
37 return x = Delta [] x [] x 38 return x = Delta [] x [] x
38 d &gt;&gt;= f = mu $ fmap f d 39 d &gt;&gt;= f = mu $ fmap f d
39 40
40 図 3: Delta に対する return と (&gt;&gt;=) の定義</blockquote> 41 図 3: Delta に対する return と (&gt;&gt;=) の定義</blockquote>
41 returnにおいては実行履歴が存在しない空の文字列を含んだMonadを返す。型aの値xは2つに複製され、異なる実行結果を得るために利用する。(&gt;&gt;=)においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。 42 returnにおいては実行履歴が存在しない空の文字列を含んだMonadを返す。型aの値xは2つに複製され、異なる実行結果を得るために利用する。(&gt;&gt;=)においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。
42 これらの関数returnと&gt;&gt;=は満たすべきMonad則が存在する。型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda[4]によって証明した。 43 これらの関数returnと&gt;&gt;=は満たすべきMonad則が存在する。型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda[4]によって証明した。
44
45 &nbsp;
43 <h5>Delta Monadにおけるプログラムの変更例</h5> 46 <h5>Delta Monadにおけるプログラムの変更例</h5>
44 変更例となるHaskellのプログラムを示す(図4)。 47 変更例となるHaskellのプログラムを示す(図4)。
45 <blockquote>generator :: Int -&gt; [Int] 48 <blockquote>generator :: Int -&gt; [Int]
46 generator x = [1..x] 49 generator x = [1..x]
47 50
76 <blockquote>generator :: Int -&gt; Delta [Int] 79 <blockquote>generator :: Int -&gt; Delta [Int]
77 generator x = let intList = [1..x] in 80 generator x = let intList = [1..x] in
78 returnD intList 81 returnD intList
79 82
80 primeFilter :: [Int] -&gt; Delta [Int] 83 primeFilter :: [Int] -&gt; Delta [Int]
81 primeFilter xs = let primeList = <span style="text-decoration: underline;">filter isPrime xs</span> 84 primeFilter xs = let primeList = <span style="text-decoration: underline;">filter isPrime xs</span>
82 modifiedList = <span style="text-decoration: underline;">filter even xs </span> in 85 modifiedList = <span style="text-decoration: underline;">filter even xs </span> in
83 returnDD primeList modifiedList 86 returnDD primeList modifiedList
84 87
85 count :: [Int] -&gt; Delta Int 88 count :: [Int] -&gt; Delta Int
86 count xs = let primeCount = length xs in 89 count xs = let primeCount = length xs in
87 returnD primeCount 90 returnD primeCount
118 <li>偶数のみを残すために2,4,6,8,10が残り</li> 121 <li>偶数のみを残すために2,4,6,8,10が残り</li>
119 <li>その個数を数えるために5となる</li> 122 <li>その個数を数えるために5となる</li>
120 </ul> 123 </ul>
121 変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。この実行結果を比較することにより、プログラムがどのように変更されたか判断する。 124 変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。この実行結果を比較することにより、プログラムがどのように変更されたか判断する。
122 今回は検証のために変更前と変更後の両方のプログラムを実行した。しかし、必ず両方実行しなくてはならない訳では無い。Haskellには遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。 125 今回は検証のために変更前と変更後の両方のプログラムを実行した。しかし、必ず両方実行しなくてはならない訳では無い。Haskellには遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
126
127 &nbsp;
123 <h5>まとめと課題</h5> 128 <h5>まとめと課題</h5>
124 Delta Monadを定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。 129 Delta Monadを定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。
125 今回定義したDelta Monadが保持できるプログラムの変更は2つまでである。Delta Monadを拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。さらに、Monadによってプログラムの変更を記述することで、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。 130 今回定義したDelta Monadが保持できるプログラムの変更は2つまでである。Delta Monadを拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。さらに、Monadによってプログラムの変更を記述することで、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。
131
132 &nbsp;
126 <h4>別刷りPDF添付</h4> 133 <h4>別刷りPDF添付</h4>
127 <a href="http://ie.u-ryukyu.ac.jp/dessertation/files/2014/10/115763K-midterm.pdf">115763K-midterm</a> 134 <a href="http://ie.u-ryukyu.ac.jp/dessertation/files/2014/10/115763K-midterm.pdf">115763K-midterm</a>
128 <h4>関連リンク</h4> 135 <h4>関連リンク</h4>
129 <ul> 136 <ul>
130 <li>Eugenio Moggi, Notion of Computation and Monads(1991)</li> 137 <li>Eugenio Moggi, Notion of Computation and Monads(1991)</li>