changeset 82:485f37d993cc

Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 28 Nov 2014 11:17:36 +0900
parents 6033d4bf54f4
children b71b93d2259f
files slides/20141128/slide.md
diffstat 1 files changed, 66 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/20141128/slide.md	Fri Nov 28 11:17:36 2014 +0900
@@ -0,0 +1,66 @@
+title: Categorical Semantics for Program Modification
+author: Yasutaka Higa
+profile:
+lang: Japanese
+
+
+# 研究目的
+* ソフトウェア開発において、プログラムが変更されることの意味を調べる
+* プログラムの変更に対応する圏を構築し、その圏の性質からプログラムの変更の性質を導く
+* 導いた性質から、プログラムの変更の意味とソフトウェア開発に使えるツールを提案する
+* 本研究ではプログラムの変更をMonadとして定義し、Monad によって構成される圏を解析する
+
+# 近況報告
+* 業務連絡 : IP filtering
+* 無限の変更を表す Delta を定義しました
+* Sample : Bubble Sort
+* Agda での証明がだいぶ詰まっています
+
+# IP filtering
+* leo.cr のみが新規?
+    * メールのIP は leo.cr, insigma.cr, firefly.cr
+    * insigma.cr, firefly.cr は登録済み
+* mumble.st, masa.cr はIPが被ってる
+
+# Delta : 当面のクリアするべき目標
+* Delta によってプログラムの全ての変更が表現できるか?
+    * Functor なのでいけると思ってます
+* 無限の変更を Delta によって書けるか
+    * 定義してみました( mono と delta )
+* Delta によって構成される limit とは何か
+    * 先生とやりました
+
+# Sample : Bubble Sort
+* prime count も bubble sort も動いてます
+
+```
+*Main>  primeCount 10
+Delta 4 (Mono 5)
+
+*Main> deltaFromList [10, 20, 30] >>= primeCount
+Delta 4 (Delta 10 (Mono 15))
+```
+
+# limit of delta monad
+* 先生と対応を考えてました
+* limit
+    * index category の形状は preorderd sets だと思ってます
+    * has id, has pull back
+    * monotone でも良いかなとは
+
+# equalizer, product of delta monnad
+* pull back があるので equalizer もある
+    * おそらく mercurial の merge の non-conflict 部分
+* id があるので product もある
+    * 任意の変更段階を対にできる
+    * parallel debugger の理論的背景 -> これを卒研の提案1にする
+* and more?
+    * indexed category のパターンを調べようかと思ってます
+
+# Agda での証明につまってます
+* functor 則は ok
+* monad 則がとんでも
+    * mu (fmap mu) m = mu (mu m)
+* 先週からずっと悩み続けてます
+
+<!-- vim: set filetype=markdown.slide: -->