# HG changeset patch # User Yasutaka Higa # Date 1424255465 -32400 # Node ID bde5e3c7de9914d03e260626be8f837c25614ff9 # Parent 32c01acbe2d38212a706b7bcc12587531daaeccf Mini fixes diff -r 32c01acbe2d3 -r bde5e3c7de99 presentation/slide.md --- a/presentation/slide.md Wed Feb 18 16:26:00 2015 +0900 +++ b/presentation/slide.md Wed Feb 18 19:31:05 2015 +0900 @@ -6,7 +6,7 @@ # 研究目的 * プログラムの信頼性を向上させる * 信頼性とはプログラムが正しく動く保証である -* 信頼性はプログラムのバグなどの原因で低下する +* プログラムの信頼性はバグなどの原因で低下する * 信頼性が低下するきっかけにプログラムの変更がある * プログラムの変更を形式化することで信頼性を保証する @@ -14,19 +14,19 @@ * Monad を用いてプログラムの変更を形式化する * プログラムにおける Monad とはメタ計算を表現するための手法である * メタ計算とは計算を実現するための計算である -* メタ計算を Delta Monad として Haskell に定義する +* プログラムの変更を表すメタ計算を Delta Monad として提案する * Delta Monad が Monad 則を満たすか Agda により証明する * Delta Monad と他の Monad の合成が可能であることを証明する # プログラムの変更の形式化 -* 形式手法とはソフトウェアの検証に数学や論理学を用いることである +* 形式手法とはソフトウェアの検証に数学や論理学を用いる手法 * Monad は圏によって形式化されている * プログラムにおいてはメタ計算の形式化に用いられる * メタ計算として変更を定義することで形式的な定義を与える * 「過去の変更を全て保存する」メタ計算 Delta Monad を提案する # プログラムの定義 -* 型付けられている値と関数のみで構成される +* 型付きの値と関数のみで構成される * プログラムの実行は関数の適用で表現できる * 関数は値としても振る舞う @@ -38,12 +38,12 @@ ``` # プログラムの変更を表現する Delta Monad -* 全ての変更を保存する +* 全ての変更を保存するメタ計算 * 変更には単位があり、変更単位をバージョンとする * ある型Aの値があった時、過去のバージョン全てを持つ ``` - T (A) = {A1, A2, A3, ... } + T A = {A1, A2, A3, ... } ``` # Haskell における Delta の定義 @@ -56,20 +56,21 @@ data Delta a = Mono a | Delta a (Delta a) ``` -# Haskell における Delta Monad の定義 +# Haskell におけるメタ計算の定義 * Haskell においてメタ計算を定義する -* 値 : 値のバージョン毎の集合 -* 関数 : 値からバージョン毎の値の集合へのマッピング -* 関数適用 : バージョンごとに関数適用する +* Delta Monad により表現されるプログラムでは + * 値 : 値のバージョン毎の集合 + * 関数 : 値からバージョン毎の値の集合へのマッピング + * 関数適用 : バージョンごとに関数適用する -# Haskell における Monad のinstance 定義 -* 関数の適用をメタ計算を行なう関数 ``>>=`` として定義 +# Haskell における Monad の instance 定義 +* 関数の適用をメタ計算を行なう中置関数 ``>>=`` として定義 * return はメタ計算に値を対応させる関数 ``` instance Monad Delta where - return x = Mono x - (Mono x) >>= f = f x + return x = Mono x + (Mono x) >>= f = f x (Delta x d) >>= f = Delta (headDelta (f x)) (d >>= (tailDelta . f)) ``` @@ -109,25 +110,25 @@ * 変更を含めて実行できるので、全てのバージョンを同時に実行できる ``` -*Main> numberCount 1000 +*Main> numberCount 1000 Delta 500 (Mono 168) ``` # 他の Monad との組み合せ * Delta Monad 以外にもメタ計算は Monad として提供されている * 例外機構、ロギング、入出力など -* 他の Monad と組み合せることにより変更に対する処理が可能 +* 他の Monad と組み合せることにより変更に対する計算が定義できる # Writer Monad と組み合せる -* ログを取る Writer Monad と組み合せた numberCount +* ログを取る Writer Monad と組み合せた numberCount の実行結果 ``` DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]", - "[2,3,5,7]", - "4"])) + "[2,3,5,7]", + "4"])) (Mono (Writer (5, ["[1,2,3,4,5,6,7,8,9,10]", - "[2,4,6,8,10]", - "5"])))) + "[2,4,6,8,10]", + "5"])))) ``` # Delta による信頼性向上手法