\documentclass{ipsjpapers}
\usepackage{url}
\usepackage[dvipdfmx]{graphicx}


% ユーザが定義したマクロなど．
\makeatletter
\let\@ARRAY\@array \def\@array{\def\<{\inhibitglue}\@ARRAY}
\def\<{\(\langle\)\nobreak}
\def\>{\nobreak\(\rangle\)}
\def\|{\verb|}
\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\LATEX{\iLATEX\Large}
\def\LATEx{\iLATEX\normalsize}
\def\LATex{\iLATEX\small}
\def\iLATEX#1{L\kern-.36em\raise.3ex\hbox{#1\bf A}\kern-.15em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}
\def\LATEXe{\ifx\LaTeXe\undefined \LaTeX 2e\else\LaTeXe\fi}
\def\LATExe{\ifx\LaTeXe\undefined \iLATEX\scriptsize 2e\else\LaTeXe\fi}
\def\Quote{\list{}{}\item[]}
\let\endQuote\endlist
\def\TT{\if@LaTeX@e\tt\fi}
\def\CS#1{\if@LaTeX@e\tt\expandafter\string\csname#1\endcsname\else
    $\backslash$#1\fi}

%\checklines    % 行送りを確認する時に使用
\begin{document}%{
% 和文表題
\title{卒業研究を通して形式手法を学んで}
% 英文表題
\etitle{}
% 所属ラベルの定義
\affilabel{ie-ryukyu}{琉球大学工学部情報工学科 \\ Department of Information Engineering, University of the Ryukyus.}
% 和文著者名
\author{比嘉 健太\affiref{ie-ryukyu} \and
        河野 真治\affiref{ie-ryukyu}}
% 英文著者名
\eauthor{Yasutaka Higa\affiref{ie-ryukyu}\and
        Shinji Kono\affiref{ie-ryukyu}}

% 和文概要
\begin{abstract}
卒業研究において形式手法を用いて問題を形式化した．
この一年間でどのようなことを行なったか，どう感じたか述べる．
\end{abstract}
% 英文概要
\begin{eabstract}

\end{eabstract}

% 表題などの出力
\maketitle

%}{

% 本文はここから始まる
\section{自己紹介}
私は琉球大学工学部情報工学科に所属する四年次の学生だ．
自動でプログラムのバグを見付ける機構が欲しいと思い，卒業研究はそのようなテーマに取り組んでいる．
卒業研究において形式手法を用いて形式化することとなったのでその経緯と感想を述べたい．

\section{卒業研究と型とAgda}
私の初期の研究テーマはプログラムから自動でバグを指摘する機構を作ることであった．

研究を進めるにつれ，プログラムのバグを見付けるには仕様やテストを記述する必要があることを知った．
テストを記述するコストはおそらくプログラムを書くコストと同じかそれ以上かかる．
あくまで私はプログラムのみでバグを見付けたかった．
そのために，プログラムの変更に着目することによりバグを見付ける手法を提案することとなった．

そこで問題となったのがプログラムの変更の表現だった．
この問題に対し，指導教員からプログラムに対する変更を Monad によって形式化するアイデアを頂いた．

Monad はプログラミング言語 Haskell では型クラスとして用意されており，型とは何かを知る必要があった．
そこで，Proofs and Types を指導教員と読むこととなった．
Proofs and Types では型と論理の対応について知ることができた．
特に自然演繹は直感的に理解でき，対応する型は私の関心の対象となった．
直感的に理解できたのは型を持つプログラミング言語を記述したことがあるのも大きい．

Proofs and Types の例題は証明支援系言語 Agda によって記述した．
Agda では項の定義とその書き換えによる等式変形を意識することとなった．
Agda における証明は依存型で記述される．
依存型を記述する言語の経験は無く，慣れるまでに時間が必要だった．
あくまで等式の変形であることに気付くまでは依存型の趣旨が全く理解できなかった．

型の理論背景を知った後，次に Monad とは一体何か知る必要があった．
Monad は圏論を元に計算機科学へ提案された表現であり，圏論を学ぶこととなった．
Monad の理解に必要な圏や関手，自然変換などを学んだが，その解釈にも私は型を用いた．
特に， Monad には満たすべき Monad 則が存在するが，依存型で表現してしまえば私にとって型に見えた．

型の理論背景と Monad を学んだ私は当初のアイデアであるプログラムに対する変更を Monad で表現することにした．
Monad という指針が存在したため，プログラムの変更を Monad として定義することができた．
特に，具体的にどのような則を満たすような型を定義すると良いか，という指針を得られたのは大きい．

\section{卒業研究を通して形式手法に思うこと}
形式手法に関して，私の卒業研究を通して得た知見は2つある．

まず1つめは形式手法を直接用いるためには専門家が必須なことである．
形式手法の提案とどのように形式化するかを指摘するには必須な知識が多く存在する．
例えば，今回の指導教員が行なった指摘には論理や圏論やプログラングなどに造形が深い必要がある．
正直に言ってしまえば，指導教員の指摘が無ければ形式手法を用いる発想は出なかったであろう．

2つめは，システムとして確立されているのなら利用しやすかったことである．
型の理論的背景を理解せずとも，これまでにプログラムを書いた経験から型システムは問題無く利用できた．
これはプログラムを書いた経験に基づくように思われる．


\section{形式手法を広めるには}
形式手法を用いるには多くの知識が必須である．
よって，前提知識を減らしたシステムとしてより手軽に利用する方が良いと考える．

例えば，Agdaでは証明はほぼ自ら記述するが，プログラムから証明が自動で導出できれば手軽に利用できる．
型のように推論が可能であれば既存のプログラムにも適用しやすい．
まずは制約が弱くとも導入しやすいシステムとして提供し，必要に応じて制約を強くするような手法はどうだろうか．

\section{まとめ}
私は卒業研究において形式手法を用いて問題を形式化した．
その際に必須な知識は多く，形式化よりもその知識の修得に時間がかかってしまった．
しかし，形式化する中で満たすべき条件が明確化されているのは処理を考える指針となった．

また，型に対する理論的背景が無くとも型システムは直感的に理解できた．
導入が手軽なシステムとして普及させ，その後から強力な手法を適用するために制約を加えていくことで普及拡大を目指すのはどうだろうか．

%}

\end{document}