Mercurial > hg > Papers > 2015 > atton-sigse

comparison slide/slide.md @ 53:65391f6321a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add description for Delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 22 Jan 2015 10:49:27 +0900
parents 780eab85e724
children 40344cc2c590
comparison
equal deleted inserted replaced
52:780eab85e724 53:65391f6321a8
77 * Coq, ... 77 * Coq, ...
78 * 他の理論 78 * 他の理論
79 * Hoare Logic, Computational Tree Logic, ... 79 * Hoare Logic, Computational Tree Logic, ...
80 * どのようなカリキュラムが良いか? 80 * どのようなカリキュラムが良いか?
81 81
82 # Delta の詳細 82 # データ構造 Delta の定義
83 * TODO... 83 * Monad によってプログラムの変更を表す
84 * データ構造としては長さ1以上のリスト
85 * nil に相当するものが元のプログラムの値
86 * プログラムの変更は変更した後の値を List に追加する
87 * 全ての関数は Delta を返し、値は Delta によって定義する
88
89 ```
90 data Delta a = Mono a | Delta a (Delta a)
91 ```
92
93 # Delta に対する Monad の instance 定義
94 * return はバージョンが無いプログラムをバージョン1とする
95 * ``>>=`` は同じバージョンの値に対する計算を同時に行なう
96
97 ```
98 instance Monad Delta where
99 return x = Mono x
100 (Mono x) >>= f = f x
101 (Delta x d) >>= f = Delta (headDelta (f x))
102 (d >>= (tailDelta . f))
103 ```
104
105 # 元のプログラムとプログラムの変更
106 ![original_program](pictures/original_program.svg)
107
108 # Delta によって記述されたプログラムの実行
109 ![delta_program](pictures/delta_program.svg)
110
111 # Delta のメリット
112 * 全てのバージョンを同時に実行できる
113 * 任意のバージョンの組み合せを同時に実行できる
114 * デバッグに利用したり 通常系/検証系 として動かす
115 * Monad なので Category との対応がある
116 * 2 つのバージョンを選ぶことは Delta が持つプログラムの product
117 * 任意のバージョンを生成できる Colimit は Program の Repository
84 118
85 <style> 119 <style>
86 .slide.cover H2 { 120 .slide.cover H2 {
87 margin-top:72px; 121 margin-top:72px;
88 font-size:72px; 122 font-size:72px;