# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1422348983 -32400
# Node ID 545c3b91479e930acf758951ec8ce11811b3f66f
# Parent  9de4706401368bc2b82fde01147306f4a49ee89c
Add slide for seminar

diff -r 9de470640136 -r 545c3b91479e slides/20150127/slide.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20150127/slide.md	Tue Jan 27 17:56:23 2015 +0900
@@ -0,0 +1,33 @@
+title: Categorical Formalization of Program Modification
+author: Yasutaka Higa
+profile:
+lang: Japanese
+
+
+# 研究目的 (Categorical Formalization)
+* プログラムの信頼性を向上させるために開発手法に着目する
+* プログラムの信頼性が変化するのはプログラムを変更した時である
+* 信頼性を保ちながらプログラムを変更にプログラムの変更を形式化する
+
+# 研究目的 (Parallel Debugger)
+* 本研究では Monad を用いてプログラムの変更を定義する
+* Monad とは meta computation とデータ構造を対応付ける手法である
+* プログラムの変更は変更前の動作を保存しつつ変更後の動作を追加することで表現する
+* 異なるバージョンのプログラムを同時に実行し、トレースを比較することでデバッグを支援する手法を提案する
+
+# 現状報告
+* 伊東の出張はもう書類は必要ない旨確認しました
+* Delta with Monad の証明
+    * 数を固定しないと無理なことが分かりました
+* 数を持つ Delta を再証明中
+
+# 数を固定しないといけない理由
+* monad の unity-law の1つ : mu . eta == id
+* eta は A -> T A なので
+    * Delta で無い value には version 1 を付与
+    * mu すると version が1しか無いので T A が1つになってしまう
+* non-Delta であれば 1, Delta n であれば n になるように A -> T A しなくてはいけない
+    * 長さ付きにしてみてますが証明難航中
+
+
+<!-- vim: set filetype=markdown.slide: -->