Binary file sigse.pdf has changed

--- a/sigse.tex	Wed Dec 24 13:15:28 2014 +0900
+++ b/sigse.tex	Wed Dec 24 16:13:47 2014 +0900
@@ -38,15 +38,14 @@
         Shinji Kono\affiref{ie-ryukyu}}
 
 \begin{abstract}
-形式手法を広めるには，手軽に何度も試行できるようにするのが重要だと思っています．
-試行を繰り返すことにより，問題の変換や詳細の把握，問題の分割などが行なえるからです．
+形式手法を広めるには，手軽に何度も試行可能であることが重要だと思っています．
+試行を繰り返すことにより，問題の変換や詳細の把握，問題の分割などが行なえるためです．
 さらに，試行のたびに必要なコストや必要な情報などを提示できれば，試行の繰り返しによりコストの最適化なども行なえます．
 また，試行を繰り返すことの重要性を指摘するに至った，私が形式手法を学び始めた1年ほどの過程を述べます．
 \end{abstract}
 
 % 表題などの出力
 \maketitle
-TODO: 研究の内容
 
 %}{
 
@@ -65,14 +64,22 @@
 
 例題の記述にはプログラミング言語 Haskell を使用しています．
 まず，プログラムの変更を表すようなデータ構造 Delta を定義します．
-Delta は過去のバージョンの値を持ち，変更としてバージョンが上がるたびに値を追加します．
-プログラムが変更されても過去の値を持ち続けることにより，プログラムの変更を表す試みです．
+Delta は全ての変更時点のプログラムの値を保持します．
+プログラムの変更は Delta への新しい値の追加として表現され，Delta はプログラムのバージョンが上がるたびに保持する値が増えます．
+プログラムが変更されても変更前の値を持ち続けることにより，プログラムの変更を表す試みです．
+
 Delta は複数のバージョンの値を持つため，計算時に処理と値のバージョンの対応を判断しなくてはなりません．
-バージョンの判断に Monad を使いました．
+例えば，バージョンが3つある変数に対してバージョンが2つある関数を適用する場合，結果の変数のバージョンは3つとします．
+変数と関数のバージョンの組み合せのルールとして Monad を用いました．
 Haskell における Monad はデータ構造とメタな計算との対応付けです\cite{moggi}．
-Delta に対して関数を適用する際， Delta と関数が互いにどのような数のバージョンを持っていても結果が一意になるよう， $ \mu $  と  $ \eta $  を定義しました．
-一意になることの確認には Monad 則を満たすことにより確認できます．
-Delta が Monad 則を満たす証明には証明支援系言語 Agda\cite{agda} を用いました．
+バージョンの組み合せの解決はメタ計算として $ \mu $ と $ \eta $ を定義します．
+関数を適用する際に必ず $ \mu $ と $ \eta $ を用いて適用することにより，関数や値の変更時にバージョンの組み合せは気にする必要が無くなります．
+メタ計算としてバージョンの組み合せを分離することで，任意の関数や変数に対し変更を行なっても変更後のプログラムが実行できます．
+
+また，バージョンの組み合せの解決はプログラム全体で一意でなくてはなりません．
+一意で無い場合，特定の箇所のみを変更することでプログラム全体のバージョンの組み合せが変わってしまいます．
+プログラム全体における組み合せが一意になることの確認は Monad 則を満たすことにより行なえます．
+定義した $ \mu $  と  $ \eta $  が Monad 則を満たすことは証明支援系言語 Agda\cite{agda} によって証明しました．
 
 現在行なったのはDelta に対する Monad 則の証明までです．
 これからプログラムのトレースの取得と，2つのプログラムのトレースの比較をしようと思っています．
@@ -98,11 +105,12 @@
 証明を記述し，その証明が成り立っているか何度も対話的に繰り返します．
 また，等式を変形していく際に前後の文脈からどのような規則により変換されるのかを提示することもできます．
 System T における自然数の加法の結合法則が上手く記述できなかった私は，1つの等式を思い付く限り変形していました．
-変形を繰り返していくうち，加法の交換法則によって変形が可能だと提示された時に Agda による証明が理解できたように思えました．
-規則とそれから導出される証明も規則であり，それらによる等式を変形で証明を記述しているのだと思いました．
+変形を繰り返していくうち，加法の交換法則によって変形が可能だと提示されました．
+その時，Agda による証明が理解できたように思えました．
+規則とそれから導出される証明も規則であり，それらによって等式を変形することで証明を記述しているのだと理解しました．
 
 何度も等式の変形を試すことによって Agda を理解した私は，高速に何度も試行することが重要だと思っています．
-特に，Agda が対話的に実行するようなインターフェースを持っていたため，対話的に実行することは多くのメリットがあると考えます．
+特に，Agda が対話的に実行するようなものであったため，対話的に実行することは多くのメリットがあると考えます．
 例えば Agda では，規則を仮定してどのような等式変形が可能かを何度も試すことができました．
 等式変形を何度も試すことにより必要な証明を明確にすることができます．
 明確化した式をさらに定義することで，証明すべき大きな式は見失わずに必要な小さな式に分割することができます．
@@ -117,18 +125,18 @@
 また，必要な分だけを実行するのは学習コストの面以外にもメリットがあると思います．
 例えば，検証の実行コストがあります．
 検証する範囲の指定とコストを対話的に何度も提示できるのなら，払うコストに対して最大の効果が得られる範囲を探れます．
-企業のようにコストや利益の見積りを考えた上で製品を開発しなくてはならない場合，どのようなコストに対してどのような効果が得られるか判断可能であれば，形式手法の導入の検討もしやすいのでは無いかと思えます．
-さらに，必要以上に検証することを見積りによって防げるのなら，コストを最小化することも可能に思えます．
+企業のようにコストや利益の見積りを考えた上で製品を開発しなくてはならない場合，どのようなコストに対してどのような効果が得られるか判断可能であれば，形式手法の導入の検討もしやすいのではないかと思えます．
+さらに，必要以上に検証することを見積りの段階で防げるのなら，コストを最小化することも可能に思えます．
 よって形式手法を広めるには，手軽に何度も試行可能であり，必要なコストや必要な情報を提示可能であることが重要だと思います．
 
 %}
 
 \begin{thebibliography}{10}
 
+\bibitem{category} Michael Barr and Charles Wells: Category Theory for Computing Science(1989)
 \bibitem{moggi} Eugenio Moggi: Notion of Computation and Monads(1991)
-\bibitem{category} Michael Barr and Charles Wells: Category Theory for Computing Science(1989)
+\bibitem{agda} The Agda Wiki - Agda: \url{http://wiki.portal.chalmers.se/agda}
 \bibitem{proofs-and-types} Jean-Yves Girard, Paulr Taylor, Yves Lafont: Proofs and Types(1990)
-\bibitem{agda} The Agda Wiki - Agda: \url{http://wiki.portal.chalmers.se/agda}
 
 \end{thebibliography}