Members/atton/seminar_slides: slides/20150324/slide.md annotate

annotate slides/20150324/slide.md @ 97:5ea8146af2e4

Add writing slides ...

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Tue, 24 Mar 2015 21:25:45 +0900
parents
children

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

Mercurial > hg > Members > atton > seminar_slides

annotate slides/20150324/slide.md @ 97:5ea8146af2e4