Mercurial > hg > Members > atton > generated_seminar_slides
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 |
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: --> |