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: -->