# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1419495477 -32400
# Node ID bfc3fc56ad90a7eb837e89b2a10b716719e75054
# Parent  9d0c57803ca0eb7190dbf89f33126cc2fc127473
Mini fixes from kngw-san, masa-san

diff -r 9d0c57803ca0 -r bfc3fc56ad90 sigse.pdf
Binary file sigse.pdf has changed
diff -r 9d0c57803ca0 -r bfc3fc56ad90 sigse.tex
--- a/sigse.tex	Thu Dec 25 14:52:33 2014 +0900
+++ b/sigse.tex	Thu Dec 25 17:17:57 2014 +0900
@@ -38,7 +38,7 @@
         Shinji Kono\affiref{ie-ryukyu}}
 
 \begin{abstract}
-大学の講義や卒業研究を通して形式手法を学んだ一年ほどの過程やつまづき，それらに基づいた形式手法を広めるための意見を述べます．
+大学の講義や卒業研究を通して一年ほど形式手法を学んだ過程やつまづき，それらに基づいた形式手法を広めるための意見を述べます．
 \end{abstract}
 
 % 表題などの出力
@@ -52,12 +52,12 @@
 形式化された範囲で作成されたプログラムは，プログラムのみで高い信頼性を持つのが理想だと考えています．
 
 現在私はプログラムの変更を形式化する研究を行なっています．
-形式化された変更によりプログラムを変更する際，プログラムが完成に近づいているか判断することが目的です．
-現在は特定の二点間での信頼性に注目し，2つのバージョン間でのトレースの相違を指摘しようとしています．
+形式化された変更によりプログラムを変更する際，プログラムが完成に近づいているかどうか判断することが目的です．
+現在は特定の二点間での信頼性に注目し，2つのバージョン間でのトレースの相違を指摘しようと考えています．
 
-私の研究においてプログラムの変更は Monad として表現します．
+私の研究においてプログラムの変更は Monad を用いて表現します．
 Monad とは，圏においては Monad 則を満たす自然変換  $ \mu $  と  $ \eta $  と Functor T です\cite{category}．
-Monad 則を満たすような  $ \mu $  と  $ \eta $  と Functor T として，プログラムの変更を表します．
+つまり，ある法則を満たす3つの要素として，プログラムの変更を表します．
 
 例題の記述にはプログラミング言語 Haskell を使用しています．
 まず，プログラムの変更を表すようなデータ構造 Delta を定義します．
@@ -66,11 +66,11 @@
 
 Delta を用いたプログラムでは，変数は必ず Delta で記述し，関数は必ず Delta を返すようにします．
 プログラムへの変更は，関数か変数のバージョンアップとして表現し，Delta への新しい値の追加として記述します．
-そうすることにより，任意の変数もしくは関数は必ず1つ以上のバージョンを持ちます．
+その結果，任意の変数もしくは関数は必ず1つ以上のバージョンを持ちます．
 
 次にバージョンを持った関数の適用を考えます．
 関数の適用は変数と関数のバージョンの違いを考慮したルールに基づいて適用しなくてはなりません．
-例えば，バージョンが1つある変数に対してバージョンが3つある関数と2つある関数を適用する場合，結果の変数のバージョンがいくつになるか決めなくては適用することができません(図\ref{apply_function})．
+例えば，バージョン数が1つの変数に対してバージョン数が3つの関数と2つの関数を適用する場合，結果の変数のバージョン数を決めなくては適用することができません(図\ref{apply_function})．
 
 \begin{figure}[htbp]
     \begin{center}
@@ -84,12 +84,12 @@
 変数と関数のバージョンの組み合せのルールは Monad を用いて記述しました．
 Haskell における Monad はデータ構造とメタな計算との対応付けです\cite{moggi}．
 メタ計算としてバージョンの組み合せの解決を $ \mu $ と $ \eta $ により定義します．
-関数を適用する際に必ず $ \mu $ と $ \eta $ を用いて適用することにより，関数や値の変更時にバージョンの組み合せは気にする必要が無くなります．
+関数を適用する際に必ず $ \mu $ と $ \eta $ を用いて適用することにより，関数や値の変更時にバージョンの組み合せを考える必要が無くなります．
 メタ計算としてバージョンの組み合せを分離することで，任意の関数や変数に対し変更を行なっても変更後のプログラムが実行できます．
 
-また，バージョンの組み合せの解決はプログラム全体で一意でなくてはなりません．
+また，バージョンの組み合せの解決はプログラム全体に対して一意でなくてはなりません．
 一意で無い場合，特定の箇所のみを変更することでプログラム全体のバージョンの組み合せが変わってしまいます．
-プログラム全体における組み合せが一意になることの確認は Monad 則を満たすことにより行なえます．
+プログラム全体における組み合せが一意であることは Monad 則を満たすことで確認できます．
 定義した $ \mu $  と  $ \eta $  が Monad 則を満たすことは証明支援系言語 Agda\cite{agda} によって証明しました．
 
 現在行なったのはDelta に対する Monad 則の証明までです．
@@ -115,7 +115,8 @@
 Agda における証明の記述は Emacs の agda-mode で行なわれます．
 証明を記述し，その証明が成り立っているか何度も対話的に繰り返します．
 また，等式を変形していく際に前後の文脈からどのような規則により変換されるのか提示することもできます．
-System T における自然数の加法の結合法則が上手く記述できなかった私は，1つの等式を思い付く限り変形していました．
+Agda の理解が深まったと思えたのは，System T における自然数の加法の結合法則を記述した時です．
+結合法則を上手く記述できなかった私は，1つの等式を思い付く限り変形していました．
 変形を繰り返していくうち，加法の交換法則によって変形が可能だと提示されました．
 その時，Agda による証明が理解できたように思えました．
 規則とそれから導出される証明も規則であり，それらによって等式を変形することで証明を記述しているのだと理解しました．
@@ -130,13 +131,13 @@
 \section{形式手法を広めるには}
 形式手法を広めるには，手軽に何度も試行可能にするのが重要だと思っています．
 手軽に何度も試行することができれば，形式手法の学習にも役立ちます．
-理解できない部分を問い，どうするべきか対話的に答えることで，学習者は解決に必要な情報を得られます．
+学習者は理解できない部分を問い，対話的な答えから解決に必要な情報を得ます．
 必要になった部分のみ学習することで，学習コストを最小限に抑えることができると思われます．
 また，必要な分だけを実行するのは学習コストの面以外にもメリットがあると思います．
 例えば，検証の実行コストがあります．
-検証する範囲の指定とコストを対話的に何度も提示できるのなら，払うコストに対して最大の効果が得られる範囲を探れます．
-企業のようにコストや利益の見積りを考えた上で製品を開発しなくてはならない場合，どのようなコストに対してどのような効果が得られるか判断可能であれば，形式手法の導入の検討もしやすいのではないかと思えます．
-さらに，必要以上に検証することを見積りの段階で防げるのなら，コストを最小化することも可能に思えます．
+検証する範囲の指定とコストを対話的に何度も提示可能なら，払うコストに対して最大の効果が得られる範囲を探ることができます．
+企業のようにコストや利益の見積りを考えた上で製品を開発しなくてはならない場合，コスト対効果が明確であることは検討の際の指針になると思えます．
+さらに，検証範囲を対話的に指定できれば，必要以上の検証や不必要な部分の洗い出しも可能かもしれません．
 よって形式手法を広めるには，手軽に何度も試行可能であり，必要なコストや必要な情報を提示可能であることが重要だと思います．
 
 %}