# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1419408867 -32400
# Node ID a4a4f5681e5fb1b9769084d40066605345768f58
# Parent  a83ebf0ea5e82559e8beed022e0d01f3e5942d8c
Mini fixes from OC-san, arari-kun-san

diff -r a83ebf0ea5e8 -r a4a4f5681e5f sigse.pdf
Binary file sigse.pdf has changed
diff -r a83ebf0ea5e8 -r a4a4f5681e5f sigse.tex
--- a/sigse.tex	Wed Dec 24 16:13:47 2014 +0900
+++ b/sigse.tex	Wed Dec 24 17:14:27 2014 +0900
@@ -52,10 +52,10 @@
 % 本文はここから始まる
 \section{現在行なっている研究}
 プログラムの信頼性の向上は自動で行なわれるべきだと思っています．
-形式化された範囲で作成されたプログラムは，人による性質の記述無しに高い信頼性を持つのが理想だと考えています．
+形式化された範囲で作成されたプログラムは，プログラムのみで高い信頼性を持つのが理想だと考えています．
 
 現在私はプログラムの変更を形式化する研究を行なっています．
-形式化された変更によってプログラムを変更する際，プログラムが完成に近づいているかを判断することが目的です．
+形式化された変更によりプログラムを変更する際，プログラムが完成に近づいているか判断することが目的です．
 現在は特定の二点間での信頼性に注目し，2つのバージョン間でのトレースの相違を指摘しようとしています．
 
 私の研究においてプログラムの変更は Monad として表現します．
@@ -65,14 +65,16 @@
 例題の記述にはプログラミング言語 Haskell を使用しています．
 まず，プログラムの変更を表すようなデータ構造 Delta を定義します．
 Delta は全ての変更時点のプログラムの値を保持します．
-プログラムの変更は Delta への新しい値の追加として表現され，Delta はプログラムのバージョンが上がるたびに保持する値が増えます．
 プログラムが変更されても変更前の値を持ち続けることにより，プログラムの変更を表す試みです．
 
-Delta は複数のバージョンの値を持つため，計算時に処理と値のバージョンの対応を判断しなくてはなりません．
-例えば，バージョンが3つある変数に対してバージョンが2つある関数を適用する場合，結果の変数のバージョンは3つとします．
-変数と関数のバージョンの組み合せのルールとして Monad を用いました．
+Delta を用いて記述されたプログラムへの変更は，関数か変数のバージョンアップとして表現されます．
+バージョンアップは Delta への新しい値の追加として記述します．
+関数や変数に対して任意の数バージョンアップを行なうことができるため，変数に関数を適用する際にそれぞれが異なるバージョン数を持つ場合があります．
+そのため，関数の適用時には関数と変数のバージョンの対応を判断しなくてはなりません．
+例えば，バージョンが3つある変数に対してバージョンが2つある関数を適用する場合，結果の変数のバージョンは2つにするか3つにするか，といったルールが必要となります．
+変数と関数のバージョンの組み合せのルールを Monad によって記述しました。
 Haskell における Monad はデータ構造とメタな計算との対応付けです\cite{moggi}．
-バージョンの組み合せの解決はメタ計算として $ \mu $ と $ \eta $ を定義します．
+メタ計算としてバージョンの組み合せの解決を $ \mu $ と $ \eta $ により定義します．
 関数を適用する際に必ず $ \mu $ と $ \eta $ を用いて適用することにより，関数や値の変更時にバージョンの組み合せは気にする必要が無くなります．
 メタ計算としてバージョンの組み合せを分離することで，任意の関数や変数に対し変更を行なっても変更後のプログラムが実行できます．
 
@@ -103,7 +105,7 @@
 
 Agda における証明の記述は Emacs の agda-mode で行なわれます．
 証明を記述し，その証明が成り立っているか何度も対話的に繰り返します．
-また，等式を変形していく際に前後の文脈からどのような規則により変換されるのかを提示することもできます．
+また，等式を変形していく際に前後の文脈からどのような規則により変換されるのか提示することもできます．
 System T における自然数の加法の結合法則が上手く記述できなかった私は，1つの等式を思い付く限り変形していました．
 変形を繰り返していくうち，加法の交換法則によって変形が可能だと提示されました．
 その時，Agda による証明が理解できたように思えました．
@@ -117,11 +119,10 @@
 このように，問題の変換や詳細の把握，問題の分割などが行なえるため対話的実行は有用だと思っています．
 
 \section{形式手法を広めるには}
-形式手法を広めるには，手軽に何度も試行できるようにするのが重要だと思っています．
-特に，対話的な手法は一つの解決策になると思います．
-私は Agda を書き続けることで依存型に対する理解を得られましたが，書き続けるには時間が必要です．
-理解できている部分だけ実行しつつ，理解できない部分はどうするべきか対話的に聞くことで必要な情報を得ます．
-必要になった部分だけ学習することで，実行したい部分に対して必要十分な理解が得られると思います．
+形式手法を広めるには，手軽に何度も試行可能にするのが重要だと思っています．
+手軽に何度も試行することができれば，形式手法の学習にも役立ちます．
+理解できない部分を問い，どうするべきか対話的に答えることで，学習者は解決に必要な情報を得られます．
+必要になった部分のみ学習することで，学習コストを最小限に抑えることができると思われます．
 また，必要な分だけを実行するのは学習コストの面以外にもメリットがあると思います．
 例えば，検証の実行コストがあります．
 検証する範囲の指定とコストを対話的に何度も提示できるのなら，払うコストに対して最大の効果が得られる範囲を探れます．