Binary file sigse.pdf has changed

--- a/sigse.tex	Tue Dec 23 16:31:08 2014 +0900
+++ b/sigse.tex	Wed Dec 24 13:07:22 2014 +0900
@@ -38,7 +38,7 @@
         Shinji Kono\affiref{ie-ryukyu}}
 
 \begin{abstract}
-講義や卒業研究を通して形式手法を学び始めた1年ほどの過程と，その中で思ったこと TODO
+講義や卒業研究を通して形式手法を学び始めた1年ほどの過程と，その中で思ったことを述べます． -- TODO
 \end{abstract}
 
 % 表題などの出力
@@ -70,7 +70,7 @@
 一意になることの確認には Monad 則を満たすことにより確認できます．
 Delta が Monad 則を満たす証明には証明支援系言語 Agda\cite{agda} を用いました．
 
-現在進んでいるのはDelta に対する Monad 則の証明までです．
+現在行なったのはDelta に対する Monad 則の証明までです．
 これからプログラムのトレースの取得と，2つのプログラムのトレースの比較をしようと思っています．
 
 \section{Agda を学んだ流れとつまづき}
@@ -83,33 +83,39 @@
 自然演繹もルールが数個しかなく，理解するのにそれほど時間はかかりませんでした．
 しかし，Agda による証明記述はすぐには理解できませんでした．
 依存型を持つ Agda では，証明は型で記述されます．
-証明を満たす型を持つ値，というのが直感的に理解できませんでした．
+証明を満たす型を持つ値，というものが直感的に理解できませんでした．
 
-Agda の特徴を取らえられたのは System T や Sytem F を Agda で記述していた時です．
 四年次になり研究室に配属された私は，プログラムのバグを自動で検出したいと希望しました．
 そこで，Proofs and Types\cite{proofs-and-types} を読むことになりました．
 Proofs and Types ではもう一度 Curry-Howard 対応や自然演繹，それに加えて System T や System F などを学びました．
-System T における自然数の加法の結合法則を証明を記述している時，等式変形に加法の交換法則を用いました．
-この時に，規則とそれから導出される証明も規則であり，それらによる等式を変形で証明を記述しているのだと理解しました．
-理解するまでには Agda で証明を書き続ける必要がありました．
+Agda の特徴を取らえられたのは System T や Sytem F を Agda で記述していた時です．
 
-また，Agda の agda-mode で実行するたびに必要な証明が指摘されているのを見た時，対話的に実行することのメリットを感じました．
-この証明を変形するにはどの証明が必要か，などと何度も試せるからです．
-式変形を試していくうちに必要な他の証明が見えてきます．
-他の証明が必須だと思った時に新たな証明を記述していくようにしました．
-こうすることにより，証明すべき大きな式は見失わずに必要な小さな式に分割することができます．
-問題の変換や詳細の把握，問題の分割などが行なえるため対話的実行は有用だと思っています．
+Agda における証明の記述は Emacs の agda-mode で行なわれます．
+証明を記述し，その証明が成り立っているか何度も対話的に繰り返します．
+また，等式を変形していく際に前後の文脈からどのような規則により変換されるのかを提示することもできます．
+System T における自然数の加法の結合法則が上手く記述できなかった私は，1つの等式を思い付く限り変形していました．
+変形を繰り返していくうち，加法の交換法則によって変形が可能だと提示された時に Agda による証明が理解できたように思えました．
+規則とそれから導出される証明も規則であり，それらによる等式を変形で証明を記述しているのだと思いました．
+
+何度も等式の変形を試すことによって Agda を理解した私は，高速に何度も試行することが重要だと思っています．
+特に，Agda が対話的に実行するようなインターフェースを持っていたため，対話的に実行することは多くのメリットがあると考えます．
+例えば Agda では，規則を仮定してどのような等式変形が可能かを何度も試すことができました．
+等式変形を何度も試すことにより必要な証明を明確にすることができます．
+明確化した式をさらに定義することで，証明すべき大きな式は見失わずに必要な小さな式に分割することができます．
+このように，問題の変換や詳細の把握，問題の分割などが行なえるため対話的実行は有用だと思っています．
 
 \section{形式手法を広めるには}
-形式手法を広めるには対話的な手法を導入するのが良いと思っています．
+形式手法を広めるには，手軽に何度も試行できるようにするのが重要だと思っています．
+特に，対話的な手法は一つの解決策になると思います．
 私は Agda を書き続けることで依存型に対する理解を得られましたが，書き続けるには時間が必要です．
-理解できている部分だけ実行しつつ，理解できない部分はどうするべきか対話的に聞くことで必要な情報を速く得ます．
+理解できている部分だけ実行しつつ，理解できない部分はどうするべきか対話的に聞くことで必要な情報を得ます．
 必要になった部分だけ学習することで，実行したい部分に対して必要十分な理解が得られると思います．
-このことにより，形式手法を学習する時間は必要な部分だけに納まり，より試しやすいものになると思います．
-
-また，必要な分だけを実行するのは形式手法の学習コスト以外にもメリットがあると思います．
-必要な分だけを検証することにより，過剰な検証コストを防ぐことができます．
-検証の範囲と必要な条件が対話的に得られるのであれば，適切なコストで検証を行なうこともできると思います．
+また，必要な分だけを実行するのは学習コストの面以外にもメリットがあると思います．
+例えば，検証の実行コストがあります．
+検証する範囲の指定とコストを対話的に何度も提示できるのなら，払うコストに対して最大の効果が得られる範囲を探れます．
+企業のようにコストや利益の見積りを考えた上で製品を開発しなくてはならない場合，どのようなコストに対してどのような効果が得られるか判断可能であれば，形式手法の導入の検討もしやすいのでは無いかと思えます．
+さらに，必要以上に検証することを見積りによって防げるのなら，コストを最小化することも可能に思えます．
+よって形式手法を広めるには，手軽に何度も試行可能であり，必要なコストや必要な情報を提示可能であることが重要だと思います．
 
 %}