Mercurial > hg > Papers > 2015 > atton-thesis
view paper/future.tex @ 87:65fdfe9c3997
Add slide in English
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 19 Feb 2015 20:24:16 +0900 |
parents | 6f699b37dc55 |
children |
line wrap: on
line source
\chapter{まとめと今後の課題} 本研究ではプログラムの変更を Monad を用いて形式化した Delta Monad を提案した。 Delta Monad の実装例として Haskell におけるメタ計算でプログラムの変更を定義した。 Delta Monad により、複数のバージョンを持つプログラムを表現し、全てのバージョンを同時に実行した。 加えてデータ型 DeltaM を定義することで、Delta Monad が他の Monad と組み合せられることを示した。 例として Writer Monad を組み合せることで複数のバージョンを同時に実行しながら個々のトレースを得た。 トレースを比較することにより、デバッグやテストに有用な情報を提供できることを示した。 また、定義した Delta と DeltaM が Monad 則を満たすことを Agda において証明した。 課題として挙げられるのは Delta Monad により表現可能な変更の定義である。 プログラムに対する可能な変更を全て Delta Monad で表現可能である証明は行なっていない。 証明可能かを確認し、不可能ならば Delta Monad により表現できる変更を定義する。 次に、 category theory によるプログラムの変更に対する意味付けがある。 category theory では category の構造から性質を導いたり、他の category への関連を導くことができる。 プログラムの変更を Monad として表した時に持つ意味や、 category が持つ有益な性質をプログラムに適用したい。 特に、複数のプログラムを同時に実行するのは product に、全てのプログラムを生成できる Delta 全体を表す集合は colimit に関連があると考えている。