# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1418290877 -32400
# Node ID 6145fed6a470c7bcc150f06eb6e5d4c2909b12b1
# Parent  c73b1c3d88ad7d6df03e7083eb03890af579b665
Writing position paper .....

diff -r c73b1c3d88ad -r 6145fed6a470 sigse.pdf
Binary file sigse.pdf has changed
diff -r c73b1c3d88ad -r 6145fed6a470 sigse.tex
--- a/sigse.tex	Thu Dec 11 15:36:38 2014 +0900
+++ b/sigse.tex	Thu Dec 11 18:41:17 2014 +0900
@@ -27,9 +27,9 @@
 %\checklines    % 行送りを確認する時に使用
 \begin{document}%{
 % 和文表題
-\title{hoge}
+\title{卒業研究を通して形式手法を学んで}
 % 英文表題
-\etitle{hoge}
+\etitle{}
 % 所属ラベルの定義
 \affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.}
 % 和文著者名
@@ -41,8 +41,8 @@
 
 % 和文概要
 \begin{abstract}
-卒業研究までの一年間で得た形式手法への感想と理想を語ろうかと．
-
+卒業研究において形式手法を用いて問題を形式化した．
+この一年間でどのようなことを行なったか，どう感じたか述べる．
 \end{abstract}
 % 英文概要
 \begin{eabstract}
@@ -57,54 +57,69 @@
 % 本文はここから始まる
 \section{自己紹介}
 私は琉球大学工学部情報工学科に所属する四年次の学生だ．
-自動でプログラムのバグを見付ける機構が欲しいと思い，卒業研究はそのようなテーマで取り組んでいる．
+自動でプログラムのバグを見付ける機構が欲しいと思い，卒業研究はそのようなテーマに取り組んでいる．
+卒業研究において形式手法を用いて形式化することとなったのでその経緯と感想を述べたい．
+
+\section{卒業研究と型とAgda}
+私の初期の研究テーマはプログラムから自動でバグを指摘する機構を作ることであった．
 
 研究を進めるにつれ，プログラムのバグを見付けるには仕様やテストを記述する必要があることを知った．
 テストを記述するコストはおそらくプログラムを書くコストと同じかそれ以上かかる．
 あくまで私はプログラムのみでバグを見付けたかった．
-そのために，プログラムの変更に着目することによりバグを見付ける手法を提案することにした．
-
-\section{卒業研究 と Category と Agda}
-私の研究においてまず問題となったのがプログラムの変更の表現だった．
+そのために，プログラムの変更に着目することによりバグを見付ける手法を提案することとなった．
 
-そこで指導教員からプログラムに対する変更を Monad によって表現するアイデアを頂いた．
-アイデアを実現するために取った過程を示したい．
+そこで問題となったのがプログラムの変更の表現だった．
+この問題に対し，指導教員からプログラムに対する変更を Monad によって形式化するアイデアを頂いた．
 
-まず， Monad とは何かを知る必要があった．
-Monad はプログラミング言語 Haskell では型クラスとして用意されており，まず型とは何かを知ることになった．
+Monad はプログラミング言語 Haskell では型クラスとして用意されており，型とは何かを知る必要があった．
 そこで，Proofs and Types を指導教員と読むこととなった．
 Proofs and Types では型と論理の対応について知ることができた．
-例題は証明支援系言語 Agda によって記述した．
-Agda では項とその書き換えによる等式変形を意識することとなった．
+特に自然演繹は直感的に理解でき，対応する型は私の関心の対象となった．
+直感的に理解できたのは型を持つプログラミング言語を記述したことがあるのも大きい．
 
-型の整合性で記述する % TODO: もうちょい書けるがまとまらない
+Proofs and Types の例題は証明支援系言語 Agda によって記述した．
+Agda では項の定義とその書き換えによる等式変形を意識することとなった．
+Agda における証明は依存型で記述される．
+依存型を記述する言語の経験は無く，慣れるまでに時間が必要だった．
+あくまで等式の変形であることに気付くまでは依存型の趣旨が全く理解できなかった．
 
 型の理論背景を知った後，次に Monad とは一体何か知る必要があった．
-Monad は Category Theory から computer science に持ち込まれたものであった．
-そのために Category theory を知る必要があった．
-Monad には満たすべき Monad則が存在し，その証明も型によって Agda で記述できた．
+Monad は圏論を元に計算機科学へ提案された表現であり，圏論を学ぶこととなった．
+Monad の理解に必要な圏や関手，自然変換などを学んだが，その解釈にも私は型を用いた．
+特に， Monad には満たすべき Monad 則が存在するが，依存型で表現してしまえば私にとって型に見えた．
 
-型とMonad を学んだ私は当初のアイデアであるプログラムに対する変更を Monad で表現することにした．
-Monad という指針が存在したため，プログラムの変更を定義することができた．
-結果的にプログラムの変更は変更前のプログラムと変更後のプログラムを同時に実行することで表わせた．
-
-\section{産業界に形式手法を普及するには}
-形式手法の普及に対して，私の卒業研究を通して得た知見は2つある．
+型の理論背景と Monad を学んだ私は当初のアイデアであるプログラムに対する変更を Monad で表現することにした．
+Monad という指針が存在したため，プログラムの変更を Monad として定義することができた．
+特に，具体的にどのような則を満たすような型を定義すると良いか，という指針を得られたのは大きい．
 
-まず1つめは形式手法を直接用いるためには専門家が必須であることである．
+\section{卒業研究を通して形式手法に思うこと}
+形式手法に関して，私の卒業研究を通して得た知見は2つある．
+
+まず1つめは形式手法を直接用いるためには専門家が必須なことである．
+形式手法の提案とどのように形式化するかを指摘するには必須な知識が多く存在する．
+例えば，今回の指導教員が行なった指摘には論理や圏論やプログラングなどに造形が深い必要がある．
 正直に言ってしまえば，指導教員の指摘が無ければ形式手法を用いる発想は出なかったであろう．
-さらに，学習のコストが高く，修得に期間がかかる．
-私は問題一つを形式化するのに一年かかった．
-それに加え，Monad によって形式化しようとする発想には必須な知識が存在する．
-どのように形式化するのかを判断できるようになるための学習コストも必要である．
-それらのコストは非常に大きく，私の経験上一年では足りないようである．
 
-2つめは，形式手法もシステムとして確立されているのなら利用しやすかったことである．
+2つめは，システムとして確立されているのなら利用しやすかったことである．
 型の理論的背景を理解せずとも，これまでにプログラムを書いた経験から型システムは問題無く利用できた．
-つまり，形式手法を直接適用するのではなく，形式化されたシステムであれば利用は比較的容易であった．
+これはプログラムを書いた経験に基づくように思われる．
 
 
-\section{まとめ?}
+\section{形式手法を広めるには}
+形式手法を用いるには多くの知識が必須である．
+よって，前提知識を減らしたシステムとしてより手軽に利用する方が良いと考える．
+
+例えば，Agdaでは証明はほぼ自ら記述するが，プログラムから証明が自動で導出できれば手軽に利用できる．
+型のように推論が可能であれば既存のプログラムにも適用しやすい．
+まずは制約が弱くとも導入しやすいシステムとして提供し，必要に応じて制約を強くするような手法はどうだろうか．
+
+\section{まとめ}
+私は卒業研究において形式手法を用いて問題を形式化した．
+その際に必須な知識は多く，形式化よりもその知識の修得に時間がかかってしまった．
+しかし，形式化する中で満たすべき条件が明確化されているのは処理を考える指針となった．
+
+また，型に対する理論的背景が無くとも型システムは直感的に理解できた．
+導入が手軽なシステムとして普及させ，その後から強力な手法を適用するために制約を加えていくことで普及拡大を目指すのはどうだろうか．
 
 %}