Mercurial > hg > Members > atton > seminar_slides
annotate slides/20150115/slide.md @ 158:6e4a6421f168
Fix slide
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 13 Dec 2016 19:48:44 +0900 |
parents | 2ff557390ef8 |
children |
rev | line source |
---|---|
90
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 title: Categorical Formalization of Program Modification |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 author: Yasutaka Higa |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 profile: |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 lang: Japanese |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 # 研究目的 (Categorical Formalization) |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 * プログラムの信頼性を向上させるために開発手法に着目する |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 * プログラムの信頼性が変化するのはプログラムを変更した時である |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 * プログラムの変更を形式化することにより、信頼性を保ちながらプログラムを変更する |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 * Kleisli Category の Kleisli Triple と対応のある Monad によってプログラムの変更を記述する |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 # 研究目的 (Parallel Debugger) |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 * 本研究では Monad を用いてプログラムの変更を定義する |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 * Monad とは meta computation とデータ構造を対応付ける手法である |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 * プログラムの変更は変更前の動作を保存しつつ変更後の動作を追加することで表現する |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 * 異なるバージョンのプログラムを同時に実行し、トレースを比較することでデバッグを支援する手法を提案する |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 # 近況報告 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 * プロシン行ってきました |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 * 結構ジャンルはなんでもありでした |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 * 機械学習、量子コンピュータ、言語処理系、ソシャゲの解析、HPC、分散FS、etc |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 * 任意の Monad と組み合せ可能な Delta を Haskell で定義してみました |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 * 証明はまだです |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 * Agda で type constraints を書けずに止まってます |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 # 任意の Monad と組み合せ可能な Delta : DeltaM |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 * 元は MonadTrans を使おうという話でした |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 * 例として MaybeT IO a は IO Maybe a らしい |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 * DeltaT を作ると DeltaT IO a は IO (Delta a) |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 * この場合、「全ての関数は Delta を返す」を満たさない |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 * 外側に Delta があって内側が任意の Monad であれば実行できる DeltaM にしてみました |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 * DeltaM IO a は Delta (IO a) です |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 # 定義中に思ったこと |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 * Delta と定義が微妙に違います |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 * 1つの関数のバージョンが上がった時に全てのバージョンを上げないといけません |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 * function のバージョンを知ることができないから |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 * 特に Monad Wrapped value を撮る時に個数が分からない |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 * Dependent type で Delta に付属させたりすれば良いのかもしれませんが |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 * 途中の bind で m a を返さないといけないので型を合わせるためにこうしてみました |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 * meta code segment って type にそのまま mapping できるかちょっと疑問に思ったりなんだり |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 # Agda で苦戦中 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 * type constraints が書けない |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 * instance (Monad m) => Monad (DeltaM m) とか書きたい |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 * Functor を Record にすることはできましたが |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 * Functor 受けとってそれに対して fmap ができない |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 * うーん…… |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 |
2ff557390ef8
Add slide for seminar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 <!-- vim: set filetype=markdown.slide: --> |