Mercurial > hg > Members > atton > generated_seminar_slides

annotate slides/20141205/slide.md @ 104:d4e4ecc1c347

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