# HG changeset patch # User Yasutaka Higa # Date 1414318890 -32400 # Node ID de0aa29cc3d545876afba6c87767882d49359e8a # Parent 5cef251269ca96096eded0d326233d36d206c6f4 update bachelor middle draft diff -r 5cef251269ca -r de0aa29cc3d5 bachelor_middle_draft/bachelor_middle_draft.tex --- a/bachelor_middle_draft/bachelor_middle_draft.tex Sun Oct 26 16:27:15 2014 +0900 +++ b/bachelor_middle_draft/bachelor_middle_draft.tex Sun Oct 26 19:21:30 2014 +0900 @@ -2,6 +2,7 @@ \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{} @@ -56,34 +57,58 @@ % {{{ Monad の定義 -\section{プログラムの変更を表現するMonadの定義} +\section{プログラムの変更を表現するMonad} プログラング言語HaskellではMonadは型に対する型クラスとして表現される。 型クラスとは特定の型Aが特定の型クラスXに属するために必要な関数群である。 その関数群を満たした型Aを型クラスXのインスタンスであると言う。 -Monadのインスタンスにする際には関数 return と >>= を定義する必要がある。 - -型変数を持つ型 Diff を定義する(\ref{diff-monad-definition}) +Monadのインスタンスにする際には関数 return と \verb/>>=/ を定義する必要がある。 -\begin{equation} - \label{diff-monad-definition} - TODO: -- ここに型 -\end{equation} +プログラムの変更をMonadで表現するために、まず型変数を持つ型 Diff を定義した(図\ref{diff-monad-definition})。 +型変数aを持つ data 型 Diff は、データコンストラクタ Diff に対して型aを持つ変数と文字列のリストを2セット渡すことによって構成される。 +このデータコンストラクタ Diff が型aの変数を型 Diff a に変換するTに相当している。 +変数を2つ持つことができるため、片方を変更前のプログラムの計算用に、片方を変更後のプログラムの計算用に利用する。 +文字列のリストは変更前のプログラムが正しく保存されているか確認するために利用するものである。 +計算そのものに対しては影響しない。 -型Diff を Monad のインスタンスとする(\ref{diff-monad-instance-definition}) - -\begin{equation} - \label{diff-monad-instance-definition} - TODO: -- ここに instance 定義 -\end{equation} +この型Diff を Monad のインスタンスとするために return と \verb/>>=/ を定義する。(図\ref{diff-monad-instance-definition}) +TODO:ここまで また、型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} +% {{{ 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} + +% }}} % }}} @@ -103,7 +128,10 @@ 変更を無限回行なえるDiffを定義することで、プログラムに対する変更をMonadによる変更のみで表したい。 また、プログラムに対する変更がMonadによって表される場合に圏論の視点からどのような意味が捉えられるか調査したい。 -圏論で捉えた場合の性質によって、他の有益な性質などを圏論側から導出できないかといった狙いがある。 +Monadは圏論から導入された概念であり、プログラム側のMonadと圏論側のMonadは対応している。 +Diff Monad を圏論の観点で捉えることにより、Diff Monadの性質などを圏論側から導出できないかといった狙いがある。 + +ひいては、プログラムを作ることや変更することは理論的にどのような意味を持つのかを探っていきたい。 % }}} diff -r 5cef251269ca -r de0aa29cc3d5 bachelor_middle_draft/eclbkbox.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/bachelor_middle_draft/eclbkbox.sty Sun Oct 26 19:21:30 2014 +0900 @@ -0,0 +1,82 @@ +% eclbkbox.sty by Hideki Isozaki, 1992 +% Date: May 28, 1993 + +\newbox\bk@bxb +\newbox\bk@bxa +\newif\if@bkcont +\newif\ifbkcount +\newcount\bk@lcnt + +\def\breakboxskip{2pt} +\def\breakboxparindent{1.8em} + +\def\breakbox{\vskip\breakboxskip\relax +\setbox\bk@bxb\vbox\bgroup +\advance\linewidth -2\fboxrule +\advance\linewidth -2\fboxsep +\hsize\linewidth\@parboxrestore +\parindent\breakboxparindent\relax} + +% \@tempdimb: amount of vertical skip +% between the first line (\bk@bxa) and the rest (\bk@bxb) +\def\bk@split{% +\@tempdimb\ht\bk@bxb % height of original box +\advance\@tempdimb\dp\bk@bxb +\setbox\bk@bxa\vsplit\bk@bxb to\z@ % split it +\setbox\bk@bxa\vbox{\unvbox\bk@bxa}% recover height & depth of \bk@bxa +\setbox\@tempboxa\vbox{\copy\bk@bxa\copy\bk@bxb}% naive concatenation +\advance\@tempdimb-\ht\@tempboxa +\advance\@tempdimb-\dp\@tempboxa}% gap between two boxes + + +% \@tempdima: height of the first line (\bk@bxa) + fboxsep +\def\bk@addfsepht{% + \setbox\bk@bxa\vbox{\vskip\fboxsep\box\bk@bxa}} + +\def\bk@addskipht{% + \setbox\bk@bxa\vbox{\vskip\@tempdimb\box\bk@bxa}} + +% \@tempdima: depth of the first line (\bk@bxa) + fboxsep +\def\bk@addfsepdp{% + \@tempdima\dp\bk@bxa + \advance\@tempdima\fboxsep + \dp\bk@bxa\@tempdima} + +% \@tempdima: depth of the first line (\bk@bxa) + vertical skip +\def\bk@addskipdp{% + \@tempdima\dp\bk@bxa + \advance\@tempdima\@tempdimb + \dp\bk@bxa\@tempdima} + +\def\bk@line{% + \hbox to \linewidth{\ifbkcount\smash{\llap{\the\bk@lcnt\ }}\fi + \vrule \@width\fboxrule\hskip\fboxsep + \box\bk@bxa\hfil + \hskip\fboxsep\vrule \@width\fboxrule}} + +\def\endbreakbox{\egroup +\ifhmode\par\fi{\noindent\bk@lcnt\@ne +\@bkconttrue\baselineskip\z@\lineskiplimit\z@ +\lineskip\z@\vfuzz\maxdimen +\bk@split\bk@addfsepht\bk@addskipdp +\ifvoid\bk@bxb % Only one line +\def\bk@fstln{\bk@addfsepdp +\vbox{\hrule\@height\fboxrule\bk@line\hrule\@height\fboxrule}}% +\else % More than one line +\def\bk@fstln{\vbox{\hrule\@height\fboxrule\bk@line}\hfil +\advance\bk@lcnt\@ne +\loop + \bk@split\bk@addskipdp\leavevmode +\ifvoid\bk@bxb % The last line + \@bkcontfalse\bk@addfsepdp + \vtop{\bk@line\hrule\@height\fboxrule}% +\else % 2,...,(n-1) + \bk@line +\fi + \hfil\advance\bk@lcnt\@ne +\if@bkcont\repeat}% +\fi +\leavevmode\bk@fstln\par}\vskip\breakboxskip\relax} + +\bkcountfalse +