\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvips]{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
%\pagestyle{fancy}
\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
\rhead{}
\cfoot{}

\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
\setlength{\headheight}{0mm}
\setlength{\headsep}{5mm}
\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
\setlength{\textwidth}{181mm}
\setlength{\textheight}{261mm}
\setlength{\footskip}{0mm}
\pagestyle{empty}

\begin{document}
\title{Modify Program by Monad}
\author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治}
\date{}
\maketitle
\thispagestyle{fancy}

% {{{ 研究目的

\section{研究目的}
プログラムを変更するとプログラムの実行内容も変更される。
その際、変更前のプログラムでは正しく実行できていた内容が変更によって損なわれる場合がある。
プログラムの変更を Monad によって行なうことにより、変更前のプログラムも保存しながらプログラムを変更する。

さらに、プログラムの変更を Monad によって定義することにより、プログラムを変更することの意味や性質などを解析する。

% }}}

% {{{ Monad

\section{Monad}
Monad とはプログラムのメタ計算に対応するもの\cite{moggi}である。

プログラムのデータは型に所属しており、関数は型から型への射と考える。
その際、任意の型Aを内包する型Tを定義することができる。
型Aを内包した型Tを T A と記述する。

特定の条件下において、型Aから型Bに変換する関数fを考えた時に、型 T A から型 T B に変換する関数 T f との対応が存在する。
ここで、f を T f に変換する際に特定の計算を追加することができ、T の定義時に決めることができる。
このことにより、型Aのデータに対して型Aから型Bに変換する関数fを適用するプログラムを、型T A のデータに対して型T Aから型T Bに変換する関数 T f のプログラムに変換することによって、変換前の処理に加えて型Tの定義時の計算を行なうことができる。

この特定の条件がMonad則であり、Monad則を満たす型TをMonadと呼ぶ。
Monadである型Tは変換前の計算に加えて型Tによって定義された計算を行なうことができる性質がある。
型Tによって追加される計算部分をメタ計算として定義し、プログラム全体のデータと関数を Monad によって記述することによりメタ計算を関数適用時に実行する。

% }}}

% {{{ Monad の定義

\section{プログラムの変更を表現するMonadの定義}
プログラング言語HaskellではMonadは型に対する型クラスとして表現される。
型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。
その関数群を満たした型Aを型クラスXのインスタンスであると言う。
Monadのインスタンスにする際には関数 return と >>= を定義する必要がある。

型変数を持つ型 Diff を定義する(\ref{diff-monad-definition})

\begin{equation}
    \label{diff-monad-definition}
    TODO: -- ここに型
\end{equation}

型Diff を Monad のインスタンスとする(\ref{diff-monad-instance-definition})

\begin{equation}
    \label{diff-monad-instance-definition}
    TODO: -- ここに instance 定義
\end{equation}

また、型Diffが Monad則(\ref{haskell-monad-law})を満たしていることをAgdaによって証明した。

\begin{eqnarray}
    \label{haskell-monad-law}
    \verb/ return a >>= k  =  k a / \\ \nonumber
    \verb/ m >>= return    =  m / \\ \nonumber
    \verb/ m >>= (\\x -> k x >>= h)  =  (m >>= k) >>= h /
\end{eqnarray}


% }}}

\section{Diff Monadを用いたプログラムの実行}
TODO: 実行例


% {{{ まとめと課題

\section{まとめと課題}
Monad によるプログラムの変更を行なった。
このことにより、変更前のプログラムを保存しながら変更後のプログラムとして実行することが可能となった。

課題としては大きく2つある。変更の個数の拡張と Monad によってプログラムを変更することの意味論を調べることである。
現状の Diff Monad はプログラムの変更を1つまでしか持つことができない。
変更を無限回行なえるDiffを定義することで、プログラムに対する変更をMonadによる変更のみで表したい。

また、プログラムに対する変更がMonadによって表される場合に圏論の視点からどのような意味が捉えられるか調査したい。
圏論で捉えた場合の性質によって、他の有益な性質などを圏論側から導出できないかといった狙いがある。

% }}}

\begin{thebibliography}{9}

\bibitem{moggi} Notion of Computation and Monads(TODO:あとで)

\end{thebibliography}
\end{document}