Mercurial > hg > Members > atton > seminar_slides

comparison slides/20141205/slide.md @ 84:faff7abdf14b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 05 Dec 2014 10:58:29 +0900
parents
children
comparison
equal deleted inserted replaced
83:b71b93d2259f 84:faff7abdf14b
1 title: Categorical Formalization for Program Modification
2 author: Yasutaka Higa
3 profile:
4 lang: Japanese
5
6
7 # 研究目的 (Categorical Formalization for Program Modification)
8 * プログラムの信頼性を向上させたい
9 * プログラムの信頼性が変化するのはプログラムを変更した時である
10 * プログラムを変更する際に信頼性を保ったまま変更するための手法を確立させたい
11 * プログラムとその変更を表すモデルとして、圏を用いる
12
13 # 研究目的 (Parallel Debugger)
14 * 本研究ではプログラムの変更を Monad として定義する
15 * Monad とは meta computation と対応付けられたデータ構造である
16 * Monad の性質を用いて、異なるバージョンを同時に実行するデータ構造Deltaを定義する
17 * 異なるバージョンの実行結果を比較することによってデバッグを支援する手法を提案する
18
19 # 近況報告
20 * 業務連絡 : プロシン申し込みました
21 * 無限の変更を表せる Delta の証明ができました
22 * Category の方の Monad則
23
24 # 業務連絡 : プロシン申し込み
25 * プロシン申し込みました
26 * 事務から書類貰ってきました
27 * 講座への振込依頼書
28 * 12/9 - 12/11 なので 12/8 - 12/11 の予定です
29
30 # Prove monad laws in Category for Delta
31 * とりあえずベタに書きました
32 * record とか使ってない
33 * Functor, Natural Transformation
34 * 先週話を聞いた後にいけそうなのでつっ走りました
35
36 # Delta の証明のキモ
37 * bind : (Delta a) -> (a -> Delta b) -> (Delta b)
38 * f と x のバージョン数が違うかもしれないので合わせる必要がある
39 * bind そのものは
40 * 関数のバージョン数
41 * 適用する変数のバージョン数
42 * が分からないけれど合わせないといけない
43
44 # Delta の証明のキモ : x = 1 , f = 1
45 * bind : (Delta a) -> (a -> Delta b) -> (Delta b)
46
47 ```
48 var = [x]
49 func = [f]
50
51 func(var) = [f(x)]
52 ```
53
54 # Delta の証明のキモ : x = 2 , f = 1
55 * bind : (Delta a) -> (a -> Delta b) -> (Delta b)
56
57 ```
58 var = [x, y]
59 func = [f]
60
61 func(var) = [f(x), f(y)]
62 ```
63
64 # Delta の証明のキモ : x = 1 , f = 2
65 * bind : (Delta a) -> (a -> Delta b) -> (Delta b)
66
67 ```
68 var = [x]
69 func = [f, g]
70
71 func(var) = [f(x), g(x)]
72 ```
73
74 # Delta の証明のキモ : x = 2 , f = 2
75 * bind : (Delta a) -> (a -> Delta b) -> (Delta b)
76
77 ```
78 var = [x, y]
79 func = [f, g]
80
81 func(var) = [[f(x), g(x)],
82 [f(y), g(y)]]
83 ```
84
85 # Delta の証明のキモ : x = 3 , f = 2
86 * bind : (Delta a) -> (a -> Delta b) -> (Delta b)
87
88 ```
89 var = [x, y, z]
90 func = [f, g]
91
92 func(var) = [[f(x), g(x)],
93 [f(y), g(y)],
94 [f(z), g(z)]]
95 ```
96
97 # Delta の証明のキモ : x = 2 , f = 3
98 * bind : (Delta a) -> (a -> Delta b) -> (Delta b)
99
100 ```
101 var = [x, y]
102 func = [f, g, h]
103
104 func(var) = [[f(x), g(x), h(x)],
105 [f(y), g(y), h(y)]]
106 ```
107
108 # Delta の証明のキモ : x = n , f = n
109 ```
110 bind (Mono x) f = f x
111 bind (Delta x d) f = Delta (headDelta (f x))
112 (bind d (tailDelta . f))
113 ```
114
115 * 自然数回分だけ tailDelta が行なわれる
116 * tailDelta の回数を自然数回適用する equiv を定義したらいけました
117 * 発想が出たのは展開するごとに tailDelta が増えるのを見たので
118
119 # Delta の証明 : Monad-laws
120 * 特に TTT に対する Monad-law
121 * mu (mu TTT) == mu (fmap mu TTT)
122 * 先程のやつの三次元版
123 * 足りない情報は bind で埋める
124 * どこからなぞっても unique ってことと同義に思える
125
126 # TODO
127 * ポジションペーパ
128 * どっちを書こうか
129 * parallel debuggerだと思ってます
130 * (P) Monad-laws in Haskell
131 * (P) MonadTransform
132 * (C) Universal Mapping Problem
133 * (C) Functor with Save Limit
134
135 <!-- vim: set filetype=markdown.slide: -->