title: プログラムの変更の圏による形式化
author: Yasutaka Higa
profile : 琉球大学工学部 <br> 情報工学科 <br> 並列信頼研究室(河野研)
lang: Japanese

# 研究目的 : プログラムの変更の形式化
* プログラムの信頼性を向上させる
* 信頼性とはプログラムが正しく動く保証である
* プログラムの信頼性はバグなどの原因で低下する
* 信頼性が低下するきっかけにプログラムの変更がある
* プログラムの変更を形式化することで信頼性を保証する

# 研究目的 : Monad を用いた変更の形式化
* Monad を用いてプログラムの変更を形式化する
* プログラムにおける Monad はメタ計算を表現するために用いる
* メタ計算とは計算を実現するための計算である
* プログラムの変更を表すメタ計算を Delta Monad として提案する
* Delta Monad が Monad 則を満たすか Agda により証明する
* Delta Monad と他の Monad の合成が可能であることを証明する

# プログラムの変更の形式化
* 形式手法とはソフトウェアの検証に数学や論理学を用いる手法
* 論理と対応する lambda 計算を用いたプログラムの形式化などがある
* Moggi らによれば圏論のMonad は関数とメタ計算を含む関数との対応
* メタ計算として変更を定義することで形式的な定義を与える
* 「過去の変更を全て保存する」メタ計算 Delta Monad を提案する

# プログラムの定義
* 型付きの値と関数のみで構成される
* プログラムの実行は関数の適用で表現できる
* 関数は値としても振る舞う

```
    x    :: A
    f    :: A -> B
    f(x) :: B
    g    :: A -> (A -> B) -> B
```

# プログラムの変更を表現する Delta Monad
* 全ての変更を保存するメタ計算
* 変更には単位があり、変更単位をバージョンとする
* ある型Aの値があった時、過去のバージョン全てを持つ

```
    T A = {A1, A2, A3, ... }
```

# Haskell における Delta の定義
* Haskell でデータ構造 Delta を作る
* リストのように順序付きの構造を持つ
* バージョン1の値は Mono
* 変更する時は Delta による値の追加

```
data Delta a = Mono a | Delta a (Delta a)
```

# Haskell におけるメタ計算の定義
* Haskell においてメタ計算を定義する
* Delta Monad により表現されるプログラムでは
    * 値       : 値のバージョン毎の集合
    * 関数     : 値からバージョン毎の値の集合へのマッピング
    * 関数適用 : バージョンごとに関数適用する

# Haskell における Monad の instance 定義
* 関数の適用時にメタ計算を行なう中置関数 ``>>=`` として定義
* return はメタ計算に値を対応させる関数

```
instance Monad Delta where
  return x           = Mono x
  (Mono x)    >>= f  = f x
  (Delta x d) >>= f  = Delta (headDelta (f x))
                             (d >>= (tailDelta . f))
```

# numberCount プログラム(バージョン1)

```
generator x     = [1..x]
numberFilter xs = filter isPrime xs
count xs        = length xs

numberCount x = count (numberFilter (generator x))
```

# numberCount プログラム(バージョン2)

```
generator x     = [1..x]
numberFilter xs = filter even xs
count xs        = length xs

numberCount x = count (numberFilter (generator x))
```

# Delta Monad によって変更を表現する
```
generator x     = Mono [1..x]
numberFilter xs = Delta (filter even xs)
                        (Mono (filter isPrime xs))
count x         = Mono (length x)

numberCount x = count =<< numberFilter =<< generator x
```

# 異なるバージョンを同時に実行する
* メタ計算としてプログラムの変更を表現できた
* 変更を含めて実行できるので、全てのバージョンを同時に実行できる

```
*Main> numberCount 1000
Delta 500 (Mono 168)
```

# 他の Monad との組み合せ
* Delta Monad 以外にもメタ計算は Monad として提供されている
* 例外機構、ロギング、入出力など
* 他の Monad と組み合せることにより変更に対する計算が定義できる
* Delta Monad が他の Monad と組み合わせ可能であることは証明した

# Writer Monad と組み合せる
* ログを取る Writer Monad と組み合せた numberCount の実行結果

```
*Main> numberCountM 10
DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]",
                           "[2,3,5,7]",
                           "4"]))
       (Mono  (Writer (5, ["[1,2,3,4,5,6,7,8,9,10]",
                           "[2,4,6,8,10]",
                           "5"]))))
```

# Delta による信頼性向上
* 各トレースの比較によるデバッグ
* 異なるバージョンの同時実行によるバージョン間互換
* 正常系と開発版を同時に実行できる
    * 正常版の入出力を開発版に対する入力にできる
* Version Control System に対する形式的な定義

# まとめと課題
* メタ計算によってプログラムの変更を定義できた
* メタ計算により信頼性の向上手法を提案できた
* Delta Monad が Monad 則を満たすことを Agda によって示した
* プログラムの変更を全て Delta Monad で記述できるか?
* 形式的な視点からプログラムの変更とは?
    * 同時実行は product, repository は colimit?


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