# HG changeset patch # User Yasutaka Higa # Date 1417141056 -32400 # Node ID 485f37d993cc2a1d04c0e1e85e670dd3b6c29608 # Parent 6033d4bf54f49f089f192782febcbe2b151d87e8 Add slide for seminar diff -r 6033d4bf54f4 -r 485f37d993cc slides/20141128/slide.md --- /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) +* 先週からずっと悩み続けてます + +