\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvips]{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
\usepackage{eclbkbox}
%\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 と \verb/>>=/ を定義する必要がある。

プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。
型変数aを持つ data 型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことによって構成される。
このデータコンストラクタ Diff が型aの変数を型 Diff a に変換するTに相当している。
変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。
文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。
計算そのものに対しては影響しない。

この型Diff を Monad のインスタンスとするために return と \verb/>>=/ を定義する。(図\ref{diff-monad-instance-definition})
TODO:ここまで

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

% {{{ source codes

\begin{breakbox}
\verb/ data Diff a = Diff [String] a [String] a/
\caption{型変数を持つ型 Diff の定義}
\label{diff-monad-definition}
\end{breakbox}

\begin{breakbox}
\begin{verbatim}
mu :: Similar (Similar a) -> Similar a
mu (Similar lx (Similar llx x _ _)
            ly (Similar _ _ lly y)) = \
    Similar (lx ++ llx) x (ly ++ lly) y

instance Monad Similar where
    return x = Similar [] x [] x
    s >>= f  = mu $ fmap f s
\end{verbatim}
\caption{Diff を Monad のインスタンスとして定義する}
\label{diff-monad-instance-definition}
\end{breakbox}

\begin{breakbox}
\begin{verbatim}
  return a >>= k  =  k a
  m >>= return    =  m
  m >>= (\\x -> k x >>= h)  =  (m >>= k) >>= h
\end{verbatim}
\caption{Haskell における Monad則}
\label{haskell-monad-law}
\end{breakbox}

% }}}


% }}}

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


% {{{ まとめと課題

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

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

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

ひいては、プログラムを作ることや変更することは理論的にどのような意味を持つのかを探っていきたい。

% }}}

\begin{thebibliography}{9}

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

\end{thebibliography}
\end{document}