Mercurial > hg > Papers > 2015 > atton-sigse
changeset 43:e233b786623e
Update description delta
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 25 Dec 2014 14:05:51 +0900 |
parents | 0429149051f6 |
children | 9d0c57803ca0 |
files | sigse.pdf sigse.tex |
diffstat | 2 files changed, 8 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/sigse.tex Thu Dec 25 12:18:29 2014 +0900 +++ b/sigse.tex Thu Dec 25 14:05:51 2014 +0900 @@ -38,7 +38,7 @@ Shinji Kono\affiref{ie-ryukyu}} \begin{abstract} -講義や卒業研究を通して形式手法を学んだ一年ほどの過程やつまづきと,それらに基づいて形式手法を広めるにはどうするべきか述べたいと思います. +大学の講義や卒業研究を通して形式手法を学んだ一年ほどの過程やつまづきと,それらに基づいた形式手法を広めるための意見を述べます。 \end{abstract} % 表題などの出力 @@ -64,12 +64,13 @@ Delta は全ての変更時点のプログラムの値を保持します. プログラムが変更されても変更前の値を持ち続けることにより,プログラムの変更を表す試みです. -Delta を用いて記述されたプログラムへの変更は,関数か変数のバージョンアップとして表現されます. -バージョンアップは Delta への新しい値の追加として記述します. -関数や変数に対して任意の数バージョンアップを行なうことができるため,変数に関数を適用する際にそれぞれが異なるバージョン数を持つ場合があります. -そのため,関数の適用時には関数と変数のバージョンの対応を判断しなくてはなりません. -例えば,バージョンが3つある変数に対してバージョンが2つある関数を適用する場合,結果の変数のバージョンは2つにするか3つにするか,といったルールが必要となります. -変数と関数のバージョンの組み合せのルールを Monad によって記述しました. +Delta を用いたプログラムでは,変数は必ず Delta で記述し,関数は必ず Delta を返すようにします. +プログラムへの変更は,関数か変数のバージョンアップとして表現し,Delta への新しい値の追加として記述します. +そうすることにより,任意の変数もしくは関数は必ず1つ以上のバージョンを持ちます. +次にバージョンを持った関数の適用を考えます. +関数の適用は通常の関数の適用と違い,変数と関数のバージョンの違いを考慮したルールに基づいて適用しなくてはなりません. +例えば,バージョンが3つある変数に対してバージョンが2つある関数を適用する場合,結果の変数のバージョンは2つにするか3つにするか決める必要があります. +変数と関数のバージョンの組み合せのルールは Monad を用いて記述しました. Haskell における Monad はデータ構造とメタな計算との対応付けです\cite{moggi}. メタ計算としてバージョンの組み合せの解決を $ \mu $ と $ \eta $ により定義します. 関数を適用する際に必ず $ \mu $ と $ \eta $ を用いて適用することにより,関数や値の変更時にバージョンの組み合せは気にする必要が無くなります.