Mercurial > hg > Members > atton > seminar_slides
annotate slides/20141125/slide.md @ 81:6033d4bf54f4
Add slide for seminar
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 25 Nov 2014 17:42:37 +0900 |
parents | |
children |
rev | line source |
---|---|
81
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 title: Categorical Semantics for Program Modification |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 author: Yasutaka Higa |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 profile: |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 lang: Japanese |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 # 研究目的 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 * プログラミングにおいてプログラムの変更に共ない実行結果なども変更される |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 * プログラムの変更に対応する圏を構築し、その変更の構造を調べる |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 * 圏の構造から導出される性質からソフトウェア開発に有用な仕組みを提案する |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 * 本研究ではプログラムの変更をMonadとして定義し、Monad によって構成される圏を解析する |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 # 近況報告 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 * 当面のクリアするべき目標 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 * 無限の変更を表す Delta を定義しました |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 * Sample : Bubble Sort |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 * Agda での証明がだいぶ詰まっています |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 # 研究の方向性と卒研 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 * Technical English Presentation でもうスライドを作り始めます |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 * あとポジションペーパが12月 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 * そういう意味で卒論とかの流れも確定させていきたい |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 * 特に研究目的 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 # 当面のクリアするべき目標 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 * Delta によってプログラムの全ての変更が表現できるか? |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 * Functor なのでいけると思ってます |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 * 無限の変更を Delta によって書けるか |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 * 定義してみました( mono と delta ) |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 * Delta によって構成される limit とは何か |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 * 先生とやりました |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 # Sample : Bubble Sort |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 * prime count も bubble sort も動いてます |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 ``` |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 *Main> primeCount 10 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 Delta 4 (Mono 5) |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 *Main> deltaFromList [10, 20, 30] >>= primeCount |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 Delta 4 (Delta 10 (Mono 15)) |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 ``` |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 # limit of delta monad |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 * 先生と対応を考えてました |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 * limit |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 * index category の形状は preorderd sets だと思ってます |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 * has id, has pull back |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 # equalizer, product of delta monnad |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 * pull back があるので equalizer もある |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 * おそらく mercurial の merge の non-conflict 部分 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 * id があるので product もある |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 * 任意の変更段階を対にできる |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 * parallel debugger の理論的背景 -> これを卒研の提案1にする |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 * and more? |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 * indexed category のパターンを調べようかと思ってます |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 # Agda での証明につまってます |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 * functor 則は ok |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 * monad 則がとんでも |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 * mu (fmap mu) m = mu (mu m) |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 * 金曜からずっと悩み続けてます |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 # 状況 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 * pattern match 全部展開 -> 無理 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 * (mono or delta) で TTT なので 2^3 くらいかなと |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 * delta を展開すると増えるので状態が爆発 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 * 安直にスクリプトで展開したけれど refl では押し切れない |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 * ≡-Reasoning で展開 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 * headDelta, tailDelta, deltaAppend と mu が natural transformation である証明とかが必要そう |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 * 今これでやってますが尋常じゃなく長い |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 |
6033d4bf54f4
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 <!-- vim: set filetype=markdown.slide: --> |