annotate slides/20150324/slide.md @ 76:1211e97e1569

auto-Update generated slides by script
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 27 Apr 2015 18:33:12 +0900
parents 7976efbb34c4
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
71
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Categorical Formalization of Program Modification
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 profile:
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: Japanese
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 # 研究目的 (Categorical Formalization)
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * プログラムの信頼性を向上させるために開発手法に着目する
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * プログラムの信頼性が変化するのはプログラムを変更した時である
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * 信頼性を保ちながらプログラムを変更にプログラムの変更を形式化する
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 * Kleisli Category の Kleisli Triple と対応のある Monad によってプログラムの変更を記述する
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 # 研究目的 (Parallel Debugger)
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 * 本研究では Monad を用いてプログラムの変更を定義する
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 * Monad とは meta computation とデータ構造を対応付ける手法である
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * プログラムの変更は変更前の動作を保存しつつ変更後の動作を追加することで表現する
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 * 異なるバージョンのプログラムを同時に実行し、トレースを比較することでデバッグを支援する手法を提案する
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 # 異なる型の Delta
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * 型を合わせるように書こうと思ったけれど無理でしたという話
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 * それぞれのシーケンスではやっぱり型はあってます
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 * 型情報を取ると動きました
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 # 型の変更を含む Delta
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 * 理想
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 * apply function
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 * `` (x, x') >>= (f, f') ``
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 * variable type
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 * `` (x, x') :: (Delta a) in (x :: a)``
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 * function type
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 * `` (f, f') :: a -> (Delta b) in (f :: a -> b)``
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 # 型変数を減らす?
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 * T A の中に B があっても問題無いのでは? という話
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 * data Delta a | ModifyInt Int (Delta a) | Mono a
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 * 問題 : 関数をどうするか
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 * A -> T B
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 * T B の中に (C -> D) を埋め込む?
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 * ってことは型チェック無理
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 # 型変数をその場で追加する ExistentialQuantification
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 * 型変数をその場で生成できたりします
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 `` data Delta b a = forall c. Delta a (Delta b c) | Mono a ``
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 * こうすると headDelta の型が不定になる
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 * a? b? c?
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 # 問題点
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 * tuple で考えると
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 * T A から `` (a, a') :: (A, C)`` を作る
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 * A -> T B から `` (f, f') :: (A -> B, C -> D) `` を作る必要がある
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 * C と (C -> D) の情報が完全に隠れているので推論できない
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 ...
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
7976efbb34c4 auto-Update generated slides by script
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 <!-- vim: set filetype=markdown.slide: -->