Mercurial > hg > Papers > 2015 > atton-sigse
annotate sigse.tex @ 29:6145fed6a470
Writing position paper .....
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 11 Dec 2014 18:41:17 +0900 |
| parents | c73b1c3d88ad |
| children | b19932e572b7 |
| rev | line source |
|---|---|
| 2 | 1 \documentclass{ipsjpapers} |
|
11
0863e8f0a3d6
Add figure for version combination
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
2 \usepackage{url} |
|
0863e8f0a3d6
Add figure for version combination
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
3 \usepackage[dvipdfmx]{graphicx} |
|
0863e8f0a3d6
Add figure for version combination
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
4 |
| 2 | 5 |
| 6 % ユーザが定義したマクロなど． | |
| 7 \makeatletter | |
| 8 \let\@ARRAY\@array \def\@array{\def\<{\inhibitglue}\@ARRAY} | |
| 9 \def\<{\(\langle\)\nobreak} | |
| 10 \def\>{\nobreak\(\rangle\)} | |
| 11 \def\|{\verb|} | |
| 12 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline} | |
| 13 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\} | |
| 14 \def\LATEX{\iLATEX\Large} | |
| 15 \def\LATEx{\iLATEX\normalsize} | |
| 16 \def\LATex{\iLATEX\small} | |
| 17 \def\iLATEX#1{L\kern-.36em\raise.3ex\hbox{#1\bf A}\kern-.15em | |
| 18 T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX} | |
| 19 \def\LATEXe{\ifx\LaTeXe\undefined \LaTeX 2e\else\LaTeXe\fi} | |
| 20 \def\LATExe{\ifx\LaTeXe\undefined \iLATEX\scriptsize 2e\else\LaTeXe\fi} | |
| 21 \def\Quote{\list{}{}\item[]} | |
| 22 \let\endQuote\endlist | |
| 23 \def\TT{\if@LaTeX@e\tt\fi} | |
| 24 \def\CS#1{\if@LaTeX@e\tt\expandafter\string\csname#1\endcsname\else | |
|
3
056c4b8a1f57
Wrote author, title
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
25 $\backslash$#1\fi} |
| 2 | 26 |
|
3
056c4b8a1f57
Wrote author, title
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
27 %\checklines % 行送りを確認する時に使用 |
| 2 | 28 \begin{document}%{ |
| 29 % 和文表題 | |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
30 \title{卒業研究を通して形式手法を学んで} |
| 2 | 31 % 英文表題 |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
32 \etitle{} |
| 2 | 33 % 所属ラベルの定義 |
|
3
056c4b8a1f57
Wrote author, title
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
34 \affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.} |
| 2 | 35 % 和文著者名 |
|
17
7ec73a287b63
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
36 \author{比嘉 健太\affiref{ie-ryukyu} \and |
|
3
056c4b8a1f57
Wrote author, title
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
2
diff
changeset
|
37 河野 真治\affiref{ie-ryukyu}} |
| 2 | 38 % 英文著者名 |
| 6 | 39 \eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and |
| 40 Shinji Kono\affiref{ie-ryukyu}} | |
| 2 | 41 |
| 42 % 和文概要 | |
| 43 \begin{abstract} | |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
44 卒業研究において形式手法を用いて問題を形式化した． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
45 この一年間でどのようなことを行なったか，どう感じたか述べる． |
| 2 | 46 \end{abstract} |
| 47 % 英文概要 | |
| 48 \begin{eabstract} | |
|
27
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
49 |
| 2 | 50 \end{eabstract} |
| 51 | |
| 52 % 表題などの出力 | |
| 53 \maketitle | |
| 54 | |
|
4
3c333203c8c5
Delete unknown charcode
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
3
diff
changeset
|
55 %}{ |
| 2 | 56 |
| 57 % 本文はここから始まる | |
|
27
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
58 \section{自己紹介} |
|
28
c73b1c3d88ad
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
59 私は琉球大学工学部情報工学科に所属する四年次の学生だ． |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
60 自動でプログラムのバグを見付ける機構が欲しいと思い，卒業研究はそのようなテーマに取り組んでいる． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
61 卒業研究において形式手法を用いて形式化することとなったのでその経緯と感想を述べたい． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
62 |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
63 \section{卒業研究と型とAgda} |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
64 私の初期の研究テーマはプログラムから自動でバグを指摘する機構を作ることであった． |
|
24
158ee14c3615
Adjust introduction
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
23
diff
changeset
|
65 |
|
27
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
66 研究を進めるにつれ，プログラムのバグを見付けるには仕様やテストを記述する必要があることを知った． |
|
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
67 テストを記述するコストはおそらくプログラムを書くコストと同じかそれ以上かかる． |
|
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
68 あくまで私はプログラムのみでバグを見付けたかった． |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
69 そのために，プログラムの変更に着目することによりバグを見付ける手法を提案することとなった． |
|
18
2ab39686323a
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
70 |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
71 そこで問題となったのがプログラムの変更の表現だった． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
72 この問題に対し，指導教員からプログラムに対する変更を Monad によって形式化するアイデアを頂いた． |
| 6 | 73 |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
74 Monad はプログラミング言語 Haskell では型クラスとして用意されており，型とは何かを知る必要があった． |
|
27
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
75 そこで，Proofs and Types を指導教員と読むこととなった． |
|
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
76 Proofs and Types では型と論理の対応について知ることができた． |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
77 特に自然演繹は直感的に理解でき，対応する型は私の関心の対象となった． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
78 直感的に理解できたのは型を持つプログラミング言語を記述したことがあるのも大きい． |
|
11
0863e8f0a3d6
Add figure for version combination
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
79 |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
80 Proofs and Types の例題は証明支援系言語 Agda によって記述した． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
81 Agda では項の定義とその書き換えによる等式変形を意識することとなった． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
82 Agda における証明は依存型で記述される． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
83 依存型を記述する言語の経験は無く，慣れるまでに時間が必要だった． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
84 あくまで等式の変形であることに気付くまでは依存型の趣旨が全く理解できなかった． |
|
27
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
85 |
|
ce6ce56bd414
Writing position paper ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
86 型の理論背景を知った後，次に Monad とは一体何か知る必要があった． |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
87 Monad は圏論を元に計算機科学へ提案された表現であり，圏論を学ぶこととなった． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
88 Monad の理解に必要な圏や関手，自然変換などを学んだが，その解釈にも私は型を用いた． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
89 特に， Monad には満たすべき Monad 則が存在するが，依存型で表現してしまえば私にとって型に見えた． |
|
28
c73b1c3d88ad
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
90 |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
91 型の理論背景と Monad を学んだ私は当初のアイデアであるプログラムに対する変更を Monad で表現することにした． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
92 Monad という指針が存在したため，プログラムの変更を Monad として定義することができた． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
93 特に，具体的にどのような則を満たすような型を定義すると良いか，という指針を得られたのは大きい． |
|
28
c73b1c3d88ad
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
94 |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
95 \section{卒業研究を通して形式手法に思うこと} |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
96 形式手法に関して，私の卒業研究を通して得た知見は2つある． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
97 |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
98 まず1つめは形式手法を直接用いるためには専門家が必須なことである． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
99 形式手法の提案とどのように形式化するかを指摘するには必須な知識が多く存在する． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
100 例えば，今回の指導教員が行なった指摘には論理や圏論やプログラングなどに造形が深い必要がある． |
|
28
c73b1c3d88ad
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
101 正直に言ってしまえば，指導教員の指摘が無ければ形式手法を用いる発想は出なかったであろう． |
|
c73b1c3d88ad
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
102 |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
103 2つめは，システムとして確立されているのなら利用しやすかったことである． |
|
28
c73b1c3d88ad
Writing position paper ....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
104 型の理論的背景を理解せずとも，これまでにプログラムを書いた経験から型システムは問題無く利用できた． |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
105 これはプログラムを書いた経験に基づくように思われる． |
| 6 | 106 |
| 107 | |
|
29
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
108 \section{形式手法を広めるには} |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
109 形式手法を用いるには多くの知識が必須である． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
110 よって，前提知識を減らしたシステムとしてより手軽に利用する方が良いと考える． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
111 |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
112 例えば，Agdaでは証明はほぼ自ら記述するが，プログラムから証明が自動で導出できれば手軽に利用できる． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
113 型のように推論が可能であれば既存のプログラムにも適用しやすい． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
114 まずは制約が弱くとも導入しやすいシステムとして提供し，必要に応じて制約を強くするような手法はどうだろうか． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
115 |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
116 \section{まとめ} |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
117 私は卒業研究において形式手法を用いて問題を形式化した． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
118 その際に必須な知識は多く，形式化よりもその知識の修得に時間がかかってしまった． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
119 しかし，形式化する中で満たすべき条件が明確化されているのは処理を考える指針となった． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
120 |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
121 また，型に対する理論的背景が無くとも型システムは直感的に理解できた． |
|
6145fed6a470
Writing position paper .....
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
122 導入が手軽なシステムとして普及させ，その後から強力な手法を適用するために制約を加えていくことで普及拡大を目指すのはどうだろうか． |
| 2 | 123 |
|
13
b34ce7d49a0c
Mini fixes from OC-san
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
11
diff
changeset
|
124 %} |
| 2 | 125 |
| 126 \end{document} |