title: Categorical Formalization of Program Modification
author: Yasutaka Higa
profile:
lang: Japanese


# 研究目的 (Categorical Formalization)
* プログラムの信頼性を向上させるために開発手法に着目する
* プログラムの信頼性が変化するのはプログラムを変更した時である
* 信頼性を保ちながらプログラムを変更にプログラムの変更を形式化する

# 研究目的 (Parallel Debugger)
* 本研究では Monad を用いてプログラムの変更を定義する
* Monad とは meta computation とデータ構造を対応付ける手法である
* プログラムの変更は変更前の動作を保存しつつ変更後の動作を追加することで表現する
* 異なるバージョンのプログラムを同時に実行し、トレースを比較することでデバッグを支援する手法を提案する

# 近況報告
* DeltaM の Monad の証明できました
* 卒論の目次を一旦書いてみました

# Delta の証明
* Delta の定義をちょっと変えました
    * 全ての Delta が同じバージョンを持つ
    * 無限の変更は対応しています
* record で書いてるのは Category の Monad 則です
    * Natural Transformation(eta, mu), unity-law, association-law
    * bind は無し

# DeltaM の証明
* 全ての Delta のバージョンが1以上かつ同じであれば DeltaM も Monad でもある
    * 中の Monad は Functor と Monad である必要がある
    * preserve-id, covariant, natural termination of eta and mu, unity-law, association-law
* 変更数は無限です
    * 若干 Functor に証明を追加しました

# fmap-equiv
* fmap する function が refl でも変換できない
* fmap-equiv として Functor の record に関数変換用の法則を追加
    * fmap-equiv : (f == g) -> (fmap f x == fmap g x)
    * Relation.Binary.PropositionalEquality に cong-app があるので良いかと判断
    * cong-app : (f == g) -> f x == g x
* higher-order function の equivalence ってあります?

# tips
* DeltaM は実際 Delta (M A) の wrapper
* constructor は 1 つなので isomorphic に対応する
    * 外す処理が必須でした
* mu を実行する時は一旦外して Deltaのmu, Inner Monad のmu
* termination checking を回避するためになるべく展開しておいた方が良かった
* Monad を合成する処理を Monad として書いてる感じが

<!-- vim: set filetype=markdown.slide: -->