Mercurial > hg > Papers > 2015 > atton-thesis
annotate paper/future.tex @ 66:f15155ec9bd9 prepaper_v1
Add generated prepaper PDF
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 17 Feb 2015 12:28:35 +0900 |
| parents | 5c6f6d7b5bb5 |
| children | 6f699b37dc55 |
| rev | line source |
|---|---|
|
23
61e5659e04a9
Add description for natural deduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
1 \chapter{まとめと今後の課題} |
| 51 | 2 本研究ではプログラムの変更を Monad を用いて形式化した。 |
| 57 | 3 特にプログラミング言語 Haskell において Delta Monad としてプログラムの変更を保存するメタ計算を実装した。 |
| 4 変更を保存するメタ計算により、複数のバージョンを持つプログラムを表現でき、複数のバージョンを持つプログラムを同時に実行した。 | |
| 5 加えて Delta Monad は DeltaM を用いて Monad と組み合せることができる。 | |
| 51 | 6 DeltaM を用いたプログラムでは複数のバージョンを持つプログラムがそれぞれどのような過程で実行されたかのトレースを得ることができた。 |
| 7 トレースを比較することにより、デバッグやテストに有用な情報を提供することができる。 | |
| 8 さらに Delta と DeltaM が Monad 則を満たすことを Agda において証明した。 | |
| 9 | |
| 10 今後の課題は大きく分けて2つが挙げられる。 | |
| 11 まず1つめはメタ計算のさらなる定義である。 | |
| 12 本研究ではプログラムの変更に対応するメタ計算として過去のプログラムを保存するメタ計算を提案した。 | |
| 13 そのメタ計算は Delta Monad として実装し、さらにメタ計算を行なう場合は Monad との組み合せとした。 | |
| 14 今回例として挙げた Monad は Writer のみであるが、他にも信頼性の向上に用いることができる Monad があると思われる。 | |
| 57 | 15 例えば変更に制約を加えるメタ計算や、バージョン毎による IO の切り分け、バージョン間の互換性などがあると考えている。 |
| 51 | 16 次に、 category theory によるプログラムの変更に対する意味付けがある。 |
| 57 | 17 category theory では category の構造から性質を導いたり、他の category への関連を導くことができる。 |
| 51 | 18 プログラムの変更を Monad として表した時に持つ意味や、 category が持つ有益な性質をプログラムに適用したい。 |
| 52 | 19 特に、複数のプログラムを同時に実行するのは product に、全てのプログラムを生成できる Delta 全体を表す集合は colimit に関連があると考えている。 |
| 64 | 20 % TODO 本当に Delta で任意の変更を表わすことができるのか |