--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/presentation/slide.md	Wed Feb 18 16:26:00 2015 +0900
@@ -0,0 +1,149 @@
+title: プログラムの変更の圏による形式化
+author: Yasutaka Higa
+profile : 琉球大学工学部 <br> 情報工学科 <br> 並列信頼研究室(河野研)
+lang: Japanese
+
+# 研究目的
+* プログラムの信頼性を向上させる
+* 信頼性とはプログラムが正しく動く保証である
+* 信頼性はプログラムのバグなどの原因で低下する
+* 信頼性が低下するきっかけにプログラムの変更がある
+* プログラムの変更を形式化することで信頼性を保証する
+
+# 研究目標
+* Monad を用いてプログラムの変更を形式化する
+* プログラムにおける Monad とはメタ計算を表現するための手法である
+* メタ計算とは計算を実現するための計算である
+* メタ計算を Delta Monad として Haskell に定義する
+* Delta Monad が Monad 則を満たすか Agda により証明する
+* Delta Monad と他の Monad の合成が可能であることを証明する
+
+# プログラムの変更の形式化
+* 形式手法とはソフトウェアの検証に数学や論理学を用いることである
+* Monad は圏によって形式化されている
+* プログラムにおいてはメタ計算の形式化に用いられる
+* メタ計算として変更を定義することで形式的な定義を与える
+* 「過去の変更を全て保存する」メタ計算 Delta Monad を提案する
+
+# プログラムの定義
+* 型付けられている値と関数のみで構成される
+* プログラムの実行は関数の適用で表現できる
+* 関数は値としても振る舞う
+
+```
+    x    :: A
+    f    :: A -> B
+    f(x) :: B
+    g    :: A -> (A -> B) -> B
+```
+
+# プログラムの変更を表現する Delta Monad
+* 全ての変更を保存する
+* 変更には単位があり、変更単位をバージョンとする
+* ある型Aの値があった時、過去のバージョン全てを持つ
+
+```
+    T (A) = {A1, A2, A3, ... }
+```
+
+# Haskell における Delta の定義
+* Haskell でデータ構造 Delta を作る
+* リストのように順序付きの構造を持つ
+* バージョン1の値は Mono
+* 変更する時は Delta による値の追加
+
+```
+data Delta a = Mono a | Delta a (Delta a)
+```
+
+# Haskell における Delta Monad の定義
+* Haskell においてメタ計算を定義する
+* 値 : 値のバージョン毎の集合
+* 関数 : 値からバージョン毎の値の集合へのマッピング
+* 関数適用 : バージョンごとに関数適用する
+
+# Haskell における Monad のinstance 定義
+* 関数の適用をメタ計算を行なう関数 ``>>=`` として定義
+* return はメタ計算に値を対応させる関数
+
+```
+instance Monad Delta where
+  return x = Mono x
+  (Mono x) >>= f     = f x
+  (Delta x d) >>= f  = Delta (headDelta (f x))
+                             (d >>= (tailDelta . f))
+```
+
+# numberCount プログラム(バージョン1)
+
+```
+generator x     = [1..x]
+numberFilter xs = filter isPrime xs
+count xs        = length xs
+
+numberCount x = count (numberFilter (generator x))
+```
+
+# numberCount プログラム(バージョン2)
+
+```
+generator x     = [1..x]
+numberFilter xs = filter even xs
+count xs        = length xs
+
+numberCount x = count (numberFilter (generator x))
+```
+
+# Delta Monad によって変更を表現する
+```
+generator x     = Mono [1..x]
+numberFilter xs = Delta (filter even xs)
+                        (Mono (filter isPrime xs))
+count x         = Mono (length x)
+
+numberCount x = count =<< numberFilter =<< generator x
+```
+
+# 異なるバージョンを同時に実行する
+* メタ計算としてプログラムの変更を表現できた
+* 変更を含めて実行できるので、全てのバージョンを同時に実行できる
+
+```
+*Main> numberCount  1000
+Delta 500 (Mono 168)
+```
+
+# 他の Monad との組み合せ
+* Delta Monad 以外にもメタ計算は Monad として提供されている
+* 例外機構、ロギング、入出力など
+* 他の Monad と組み合せることにより変更に対する処理が可能
+
+# Writer Monad と組み合せる
+* ログを取る Writer Monad と組み合せた numberCount
+
+```
+DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]",
+                            "[2,3,5,7]",
+                            "4"]))
+       (Mono  (Writer (5, ["[1,2,3,4,5,6,7,8,9,10]",
+                            "[2,4,6,8,10]",
+                            "5"]))))
+```
+
+# Delta による信頼性向上手法
+* 各トレースの比較によるデバッグ
+* 異なるバージョンの同時実行によるバージョン間互換
+* 正常系と開発版を同時に実行できる
+    * 正常版の入出力を開発版に対する入力にできる
+* Version Control System に対する形式的な定義
+
+# まとめと課題
+* メタ計算によってプログラムの変更を定義できた
+* メタ計算により信頼性の向上手法を提案できた
+* Monad であることを Agda によって示した
+* プログラムの変更を全て Delta Monad で記述できるか?
+* 形式的な視点からプログラムの変更とは?
+    * 同時実行は product, repository は colimit?
+
+
+<!-- vim: set filetype=markdown.slide: -->