Binary file bachelor_middle_draft.pdf has changed

--- a/wordpress.html	Wed Oct 29 16:24:10 2014 +0900
+++ b/wordpress.html	Wed Oct 29 16:52:52 2014 +0900
@@ -1,59 +1,134 @@
 <div>[toc]</div>
 <h4>115763K:比嘉健太</h4>
 <h4>Modify Program by Monad</h4>
-<h4>プログラムの変更を表すMonad</h4>
-プログラムを変更するとプログラムの実行結果も変化する。しかし、変更後のプログラムが正しい実行結果でない場合も存在する。そこで、プログラムに対する変更をMonadとして記述する。Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。ひいては、プログラムを変更することの意味や性質などを解析する。
+<h5>プログラムの変更を表すMonad</h5>
+プログラムを変更するとプログラムの実行結果も変化する。しかし、変更後のプログラムが正しい実行結果でない場合も存在する。そこで、プログラムに対する変更をMonadとして記述する。Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。ひいては、プログラムを変更することの意味や性質などを解析する。
+<h5>限定されたプログラムの変更を表すDelta Monad</h5>
+Monadを用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。HaskellにおけるMonadとはメタ計算を内包したデータ型である。Monadであるデータ型は任意の型の値を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。
+Haskellにおいて限定されたプログラムの変更を表すことができるDelta Monadを定義した。Delta Monadにおけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。
+データ型Deltaの定義を示す(図1)。
+<div title="Page 1">
+<div>
+<div>
+<blockquote>
+<pre>data Delta a = Delta [String] a [String] a</pre>
+図 1: 型変数を持つ型 Delta の定義 (Haskell)</blockquote>
+</div>
+</div>
+</div>
+データ型Deltaは任意の型aの変数を持つことができる。型aの変数を2つと変数に対する実行履歴となる文字列のリストを2つ持つ。このデータ型をMonadとして利用するが、あるデータ型をMonadとするためには関数returnと&gt;&gt;=を定義する必要がある(図2)。
+<div title="Page 1">
+<div>
+<div>
+<blockquote>
+<pre>return :: Monad m =&gt; a -&gt; m a
+(&gt;&gt;=) :: Monad m =&gt; m a -&gt; (a -&gt; m b) -&gt; m b</pre>
+図 2: データ型を Monad とするために必要な関数</blockquote>
+</div>
+</div>
+</div>
+図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に対するメタ計算の定義となる。
+Deltaにおけるreturnと&gt;&gt;=の定義を図3に示す。
+<blockquote>mu (Delta lx (Delta llx x _ _)
+ly (Delta _ _ lly y)) =
+Delta (lx ++ llx) x (ly ++ lly) y
 
-<h4>限定されたプログラムの変更を表すDelta Monad</h4>
-Monadを用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。HaskellにおけるMonadとはメタ計算を内包したデータ型である。Monadであるデータ型は任意の型の値を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。
-Haskellにおいて限定されたプログラムの変更を表すことができるDelta Monadを定義した。Delta Monadにおけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。
-データ型Deltaの定義を示す(図1)。
-データ型Deltaは任意の型aの変数を持つことができる。型aの変数を2つと変数に対する実行履歴となる文字列のリストを2つ持つ。このデータ型をMonadとして利用するが、あるデータ型をMonadとするためには関数returnと>>=を定義する必要がある(図2)。
-図2の定義は関数の型のみ記述している。mはMonadであり、m aは任意の型aを内包するMonadである。returnは任意の型aからm aの値を返す関数returnがある。returnは任意の型の値をMonadに内包するために利用する。中置関数(>>=)はMonadの値m aと、aを取ってm bを返す関数を取り、m bの値を返す。(>>=)の定義がMonadに対するメタ計算の定義となる。
-Deltaにおけるreturnと>>=の定義を図3に示す。
-returnにおいては実行履歴が存在しない空の文字列を含んだMonadを返す。型aの値xは2つに複製され、異なる実行結果を得るために利用する。(>>=)においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。
-これらの関数returnと>>=は満たすべきMonad則が存在する。型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda[4]によって証明した。
+instance Monad Delta where
+return x = Delta [] x [] x
+d &gt;&gt;= f  = mu $ fmap f d
 
-<h4>Delta Monadにおけるプログラムの変更例</h4>
-変更例となるHaskellのプログラムを示す(図4)。
-このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。1からnまでの整数の個数を調べるprimeCount関数は3つの関数からなる。
+図 3: Delta に対する return と (&gt;&gt;=) の定義</blockquote>
+returnにおいては実行履歴が存在しない空の文字列を含んだMonadを返す。型aの値xは2つに複製され、異なる実行結果を得るために利用する。(&gt;&gt;=)においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。
+これらの関数returnと&gt;&gt;=は満たすべきMonad則が存在する。型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda[4]によって証明した。
+<h5>Delta Monadにおけるプログラムの変更例</h5>
+変更例となるHaskellのプログラムを示す(図4)。
+<blockquote>generator :: Int -&gt; [Int]
+generator x = [1..x]
 
-<ul>
-<li>1からnまでの整数を返す関数generator</li>
-<li>整数のリストから素数である整数のみを残したリストを返す関数primeFilter</li>
-<li>リストの中に存在する要素の個数を返す関数count</li>
-</ul>
+primeFilter :: [Int] -&gt; [Int]
+primeFilter xs = filter isPrime xs
+
+count :: [Int] -&gt; Int
+count xs = length xs
+
+primeCount :: Int -&gt; Int
+primeCount x = count . primeFilter . generator $ x
 
-ここで、primeFilter関数を変更する。素数である整数を残すのではなく、偶数を残すようにする。Delta Monadを使わずにprimeFilter関数を変更すると図5のプログラムとなる。
-プログラム(図4)に対する図5の変更をDelta Monadで記述したものが図6のプログラムである。
-Delta Monadを用いたプログラムでは全ての関数はDelta Monadを返す関数として記述される。変更されるprimeFilter関数は、素数によるフィルタと偶数によるフィルタの両方の結果を持ったDelta Monadを返すよう変更する。図6のプログラムを実行した例が図7である。
-Delta Monadによる実行結果は2つの実行結果が存在する。変更前のプログラムの実行順序が上側の実行結果である。
-
-<ul>
-<li>1から10までのリストを作成し</li>
-<li>素数のみを残すために2,3,5,7が残り</li>
-<li>その個数を数えるために4となる</li>
-</ul>
-
-変更後のプログラムの実行順序が下側の実行結果である。
+図 4: 変更前の Haskell プログラム</blockquote>
+このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。1からnまでの整数の個数を調べるprimeCount関数は3つの関数からなる。
 <ul>
-<li>1から10までのリストを作成し</li>
-<li>偶数のみを残すために2,4,6,8,10が残り</li>
-<li>その個数を数えるために5となる</li>
+	<li>1からnまでの整数を返す関数generator</li>
+	<li>整数のリストから素数である整数のみを残したリストを返す関数primeFilter</li>
+	<li>リストの中に存在する要素の個数を返す関数count</li>
 </ul>
-変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。この実行結果を比較することにより、プログラムがどのように変更されたか判断する。
-今回は検証のために変更前と変更後の両方のプログラムを実行した。しかし、必ず両方実行しなくてはならない訳では無い。Haskellには遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
+ここで、primeFilter関数を変更する。素数である整数を残すのではなく、偶数を残すようにする。Delta Monadを使わずにprimeFilter関数を変更すると図5のプログラムとなる。
+<div title="Page 2">
+<div>
+<div>
+<blockquote>
+<pre>primeFilter :: Int -&gt; Int
+primeFilter xs = filter <span style="text-decoration: underline;"><span style="color: #000000; text-decoration: underline;">even</span></span> xs</pre>
+図 5: 変更後の primeFilter 関数 (変更点は下線)</blockquote>
+</div>
+</div>
+</div>
+プログラム(図4)に対する図5の変更をDelta Monadで記述したものが図6のプログラムである。
+<blockquote>generator :: Int -&gt; Delta [Int]
+generator x = let intList = [1..x] in
+returnD intList
+
+primeFilter :: [Int] -&gt; Delta [Int]
+primeFilter xs = let primeList    = <span style="text-decoration: underline;">filter isPrime xs</span>
+modifiedList = <span style="text-decoration: underline;">filter even xs </span>   in
+returnDD primeList modifiedList
+
+count :: [Int] -&gt; Delta Int
+count xs = let primeCount = length xs in
+returnD primeCount
 
-<h4>まとめと課題</h4>
-Delta Monadを定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。
-今回定義したDelta Monadが保持できるプログラムの変更は2つまでである。Delta Monadを拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。さらに、Monadによってプログラムの変更を記述することで、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。
+primeCount :: Int -&gt; Delta Int
+primeCount x = generator x &gt;&gt;= primeFilter &gt;&gt;= count
+<div title="Page 2">
+<div>
+<div>
+<div>
+
+図 6: 図 4 のプログラムに対する図 5 の変更を Delta Monad で記述した例 (対応する変更点は下線)
+
+</div>
+</div>
+</div>
+</div></blockquote>
+Delta Monadを用いたプログラムでは全ての関数はDelta Monadを返す関数として記述される。変更されるprimeFilter関数は、素数によるフィルタと偶数によるフィルタの両方の結果を持ったDelta Monadを返すよう変更する。図6のプログラムを実行した例が図7である。
+<blockquote>*Main&gt; primeCount 10
+Delta
+["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4
+["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5
 
-
-<h5>別刷りPDF添付</h5>
+図 7: Delta Monad を用いたプログラムの実行例</blockquote>
+Delta Monadによる実行結果は2つの実行結果が存在する。変更前のプログラムの実行順序が上側の実行結果である。
+<ul>
+	<li>1から10までのリストを作成し</li>
+	<li>素数のみを残すために2,3,5,7が残り</li>
+	<li>その個数を数えるために4となる</li>
+</ul>
+変更後のプログラムの実行順序が下側の実行結果である。
+<ul>
+	<li>1から10までのリストを作成し</li>
+	<li>偶数のみを残すために2,4,6,8,10が残り</li>
+	<li>その個数を数えるために5となる</li>
+</ul>
+変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。この実行結果を比較することにより、プログラムがどのように変更されたか判断する。
+今回は検証のために変更前と変更後の両方のプログラムを実行した。しかし、必ず両方実行しなくてはならない訳では無い。Haskellには遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
+<h5>まとめと課題</h5>
+Delta Monadを定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。
+今回定義したDelta Monadが保持できるプログラムの変更は2つまでである。Delta Monadを拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。さらに、Monadによってプログラムの変更を記述することで、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。
+<h4>別刷りPDF添付</h4>
+<a href="http://ie.u-ryukyu.ac.jp/dessertation/files/2014/10/115763K-midterm.pdf">115763K-midterm</a>
 <h4>関連リンク</h4>
 <ul>
-  <li>Eugenio Moggi, Notion of Computation and Monads(1991)</li>
-  <li>Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990)</li>
-  <li>Michael Barr and Charles Wells, Category Theory for Computing Science</li>
-  <li>The Agda Wiki - Agda http://wiki.portal. chalmers.se/agda/pmwiki.php</li>
+	<li>Eugenio Moggi, Notion of Computation and Monads(1991)</li>
+	<li>Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990)</li>
+	<li>Michael Barr and Charles Wells, Category Theory for Computing Science</li>
+	<li>The Agda Wiki - Agda http://wiki.portal. chalmers.se/agda/pmwiki.php</li>
 </ul>