title: プログラムのデバッグ支援(仮)
author: Yasutaka Higa
cover:
lang: Japanese



# 研究目的(仮)
* プログラミングにおいて、ソースコードを改変するとプログラムの挙動も変わる
* 挙動は予想されていた挙動と異なる場合があり、それはバグとなる
* ソースコードの改変前と改変後の挙動を比較することで、デバッグの支援になるのでは無いか
* 異なるバージョンのプログラムを同時に実行できるデバッグ支援ツールを開発する


# 近況報告
* Parallel debugger sample session
    * テコ入れ下さい
* ソフトウェア工学の質問とか答えてたりしました
* Notions of computation and monads


# ソフトウェア工学
* 数日前から質問来てました(締切前?)
* Functor の eta の記述がおかしい気がします
    * T -> 1 になってる
    * eta は 1 -> T な気がします
* [ここ](http://www.ie.u-ryukyu.ac.jp/%7Ekono/lecture/software/s05/lecture.html)の etaT のところ

# Notions of computation and monads
* proving Equivalence of programs
    * beta-eta conversion wipes out
        * non-termination, non-determinisim, side-effects
* follows monads
    * Categorical Semantics of computations based on monads
* T is notion of computation

# Many Sorted Monadic Equational Language ?
* Kleisli triples との対応
    * (T, eta, mu) と (T, eta, _ * )
    * このあたりはソフトウェア工学でやったところなのでどうにか
* Many Sorted Monadic Equational Launguage くらいから謎
    * page6-7 とか
    * 確実に引数を1つ持つ関数どうしの Equation?

# Notions of computation and monads : ながれ
* あとは流し読み
* Many sorted Monadic Equational Language -> The Simple metalanguage
    * (let とか。) 1Monad を複数回適用可能?
* A Simple Programming Language
    * existential とかが導入されるらしいですが……

# Notions of computation and monads : ながれ
* Extending the simple metalanguage
    * Strong Monad (A x T B) -> T A B
* Interpretation and formal system
* Strong monads over a topos
    * location, if とかが が入る

# Monad for CbC?
* Monad は codomain が 2つある
    * A と T A
    * なので A と T A 間での identitiy はきちんと取る必要がありそう
* f : A -> T B
    * f x     の場合は x : A
    * f =<< x の場合は x : T A

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