# HG changeset patch # User Yasutaka Higa # Date 1414569258 -32400 # Node ID 83777243f57296a20ce811b3df27184840837927 # Parent 3e1c5f2f23f22b9dacb0a1d7c1250fbccc7a9018 Submit to wordpress diff -r 3e1c5f2f23f2 -r 83777243f572 wordpress.html --- a/wordpress.html Wed Oct 29 16:52:52 2014 +0900 +++ b/wordpress.html Wed Oct 29 16:54:18 2014 +0900 @@ -1,8 +1,11 @@
[toc]

115763K:比嘉健太

Modify Program by Monad

+ 
プログラムの変更を表すMonad
プログラムを変更するとプログラムの実行結果も変化する。しかし、変更後のプログラムが正しい実行結果でない場合も存在する。そこで、プログラムに対する変更をMonadとして記述する。Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。ひいては、プログラムを変更することの意味や性質などを解析する。 + + 
限定されたプログラムの変更を表すDelta Monad
Monadを用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。HaskellにおけるMonadとはメタ計算を内包したデータ型である。Monadであるデータ型は任意の型の値を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。 Haskellにおいて限定されたプログラムの変更を表すことができるDelta Monadを定義した。Delta Monadにおけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。 @@ -29,17 +32,17 @@ 図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に示す。 -
mu (Delta lx (Delta llx x _ _) -ly (Delta _ _ lly y)) = -Delta (lx ++ llx) x (ly ++ lly) y +
mu (Delta lx (Delta llx x _ _) ly (Delta _ _ lly y)) = Delta (lx ++ llx) x (ly ++ lly) y instance Monad Delta where return x = Delta [] x [] x -d >>= f = mu $ fmap f d +d >>= f = mu $ fmap f d 図 3: Delta に対する return と (>>=) の定義
returnにおいては実行履歴が存在しない空の文字列を含んだMonadを返す。型aの値xは2つに複製され、異なる実行結果を得るために利用する。(>>=)においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。 これらの関数returnと>>=は満たすべきMonad則が存在する。型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda[4]によって証明した。 + + 
Delta Monadにおけるプログラムの変更例
変更例となるHaskellのプログラムを示す(図4)。
generator :: Int -> [Int] @@ -78,8 +81,8 @@ returnD intList primeFilter :: [Int] -> Delta [Int] -primeFilter xs = let primeList = filter isPrime xs -modifiedList = filter even xs in +primeFilter xs = let primeList = filter isPrime xs +modifiedList = filter even xs in returnDD primeList modifiedList count :: [Int] -> Delta Int @@ -120,9 +123,13 @@ 変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。この実行結果を比較することにより、プログラムがどのように変更されたか判断する。 今回は検証のために変更前と変更後の両方のプログラムを実行した。しかし、必ず両方実行しなくてはならない訳では無い。Haskellには遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。 + + 
まとめと課題
Delta Monadを定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。 今回定義したDelta Monadが保持できるプログラムの変更は2つまでである。Delta Monadを拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。さらに、Monadによってプログラムの変更を記述することで、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。 + + 

別刷りPDF添付

115763K-midterm

関連リンク