Mercurial > hg > Papers > 2015 > atton-thesis

changeset 63:c75ba6313e39

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing prepaper...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 17 Feb 2015 12:08:10 +0900
parents 36795f6b6e87
children 5c6f6d7b5bb5
files paper/delta.tex paper/main.pdf prepaper/115763K.tex prepaper/Makefile prepaper/reference.bib prepaper/src/DeltaM.hs prepaper/src/delta_data.hs prepaper/src/delta_instance_monad.hs prepaper/src/numberCount1.hs prepaper/src/numberCount2.hs prepaper/src/numberCountDelta.hs prepaper/src/numberCountResult.txt
diffstat 12 files changed, 248 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/paper/delta.tex	Tue Feb 17 10:09:22 2015 +0900
+++ b/paper/delta.tex	Tue Feb 17 12:08:10 2015 +0900
@@ -5,9 +5,9 @@
 第\ref{chapter:delta}章ではプログラムの変更を表す Delta Monad を定義し、その使用例とメタ計算の例を示す。
 なお、Monad についての定義と解説は第\ref{chapter:category}章と第\ref{chapter:functional_programming}章にて行なう。
 
-% {{{ Delta Monad の定義
-
-\section{Delta Monad の定義}
+% {{{ Monad とメタ計算
+\section{Monad とメタ計算}
+\label{section:monad_with_meta_computation}
 
 まずはプログラムを定義する。
 プログラムは型付けされた値と、値を値へと写像する関数のみで構成される。
@@ -56,6 +56,12 @@
 メタ計算が無い関数 $ f $ とメタ計算を持つ関数 $ f^{*} $ が1対1に対応することは Monad により保証されている。
 このように、値と関数で表されたプログラムにおいてメタ計算を用いることで、計算を拡張することができる。
 
+% }}}
+
+% {{{ Delta Monad の定義
+
+\section{Delta Monad の定義}
+
 プログラムとメタ計算の関係としての Monad について述べたところで、プログラムの変更をメタ計算として記述することを考える。
 
 プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。
Binary file paper/main.pdf has changed
--- a/prepaper/115763K.tex	Tue Feb 17 10:09:22 2015 +0900
+++ b/prepaper/115763K.tex	Tue Feb 17 12:08:10 2015 +0900
@@ -2,6 +2,7 @@
 \usepackage[dvips]{graphicx}
 \usepackage{picins}
 \usepackage{fancyhdr}
+\usepackage{listings}
 \pagestyle{fancy}
 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 卒業研究発表会}
 \rhead{}
@@ -17,6 +18,26 @@
 \setlength{\footskip}{0mm}
 \pagestyle{empty}
 
+
+%% listings settings
+
+\lstset{
+  frame=single,
+  keepspaces=true,
+  basicstyle={\ttfamily},
+  breaklines=true,
+  xleftmargin=0zw,
+  xrightmargin=0zw,
+  framerule=.2pt,
+  columns=[l]{fullflexible},
+  language={},
+  tabsize=4,
+  lineskip=-0.5zw,
+  escapechar={@},
+}
+\def\lstlistingname{リスト}
+
+
 \begin{document}
 \title{Categorical Formalization of Program Modification}
 \author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治}
@@ -35,10 +56,9 @@
 \end{abstract}
 
 \section{プログラムの変更の形式化}
-本研究ではプログラムの信頼性を向上させることを目的とする。
+本研究はプログラムの信頼性を向上させることを目的とする。
 信頼性とはプログラムが正しく動作する保証であり、プログラムのバグなど多くの原因により低下する。
-信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を形式化する。
-特に本研究では Monad を用いたメタ計算としてプログラムの変更を記述する。
+信頼性が変化する点としてプログラムの変更に注目し、プログラムの変更を Monad を用いたメタ計算として形式化する。
 加えて、定義した計算が Monad 則を満たすかの証明を行なう。
 
 \section{メタ計算と Monad}
@@ -47,36 +67,118 @@
 関数は値から値へ写像するものである。
 プログラムの実行は関数の適用として表される。
 この時、入出力といった値の写像のみで表現できない計算を表現するために Monad を用いる。
-プログラムにおける Monad とはデータ構造とメタ計算の関連付けであり、メタ計算とは計算を行なう計算である。
-入出力機構をプログラムの計算とは別に定義し、メタ計算とする。
-メタ計算を利用したい関数は値をメタ計算と関連付けられたデータ型へと写像する。
-プログラムを実行した結果のデータ型を元にメタ計算を実行することで、プログラムの内部ではメタ計算を扱うことなくメタ計算を実行できる。
-これが Monad を用いた計算とメタ計算の対応である。
-例えばプログラミング言語 Haskell においては、入出力処理や非決定性、失敗する可能性のある計算や例外処理などが Monad として提供されている。
+プログラムにおける Monad とはデータ構造とメタ計算の関連付けであり、メタ計算とは計算を行なう計算である ~\cite{Moggi:1991:NCM:116981.116984}。
+メタ計算として入出力機構をプログラムの計算とは別に定義し、入出力を利用したい関数は値をメタ計算と関連付けられたデータ型へと写像することで実現する。
+Monad を用いることでプログラムの内部ではメタ計算を扱わずにメタ計算を実現できる。
 
 \section{変更を表す Delta Monad}
-本研究ではプログラムの変更を表すメタ計算として、変更の時に過去のプログラムも保存するメタ計算を提案する。
-このメタ計算に対応する Monad として Delta Monad をプログラミング言語 Haskell にて実装する。
+本研究ではプログラムの変更を表すメタ計算として、変更時に過去のプログラムも保存するメタ計算を提案する。
+このメタ計算に対応する Monad として Delta Monad を定義し、プログラミング言語 Haskell にて実装する。
 Delta Monad では変更単位をバージョンとし、全てのバージョンを保存しつつ実行することができる。
-Delta Monad と対応するデータ型Delta を定義する。
+まずは、Delta Monad と対応するデータ型 Delta を定義する。
 
-TODO: source
+\begin{table}[html]
+    \lstinputlisting[label=src:delta_data, caption= Delta のデータ定義] {src/delta_data.hs}
+\end{table}
 
 バージョンが1である値はコンストラクタ Mono によって構成され、複数のバージョンを持つ場合はコンストラクタ Delta により構成される。
-Delta Monad におけるプログラムは全ての値が Delta であり、全ての関数はDeltaを返す。
-つまりプログラム全体においてバージョンは一意である。
+よって、最初のプログラムにおける値は Mono で構成され、値の変更を行なう時は Delta を追加することで表現する。
+そのためバージョンによって順序付けられたリストが構成される。
+
+次に Delta 型と関連付けるメタ計算を示す。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:delta_instance_monad, caption= Delta に対するメタ計算の定義] {src/delta_instance_monad.hs}
+\end{table}
+
+Delta Monad では全てのバージョンのプログラムを保存し、同時に実行できるメタ計算を実現する。
+プログラムはバージョンによって順序付けられているため、計算する際にバージョンが同じ関数と値を用いて関数を適用することで実現する。
+コンストラクタが Mono であった場合はバージョン1であるため、バージョン1どうしの計算を行なう。
+バージョンが1より大きい Delta で構成される場合は、先頭のバージョンどうしを計算し、先頭を除いた形に変形してから再帰的にメタ計算を適用する。
+
+\section{Delta Monad を用いたプログラムの例}
+Delta Monad を用いてプログラムの変更を記述する。
+
+まずは変更前のプログラム numberCount を示す。
 
-TODO: temporary......
+\begin{table}[html]
+    \lstinputlisting[label=src:numberCountV1,
+                     caption= numberCount プログラムバージョン1,
+                     basicstyle={\small}] {src/numberCount1.hs}
+\end{table}
+
+numberCount プログラムは、1 から n の整数において特定の数の個数を数えるプログラムである。
+プログラムは3つの関数によって表現される。
+\begin{itemize}
+    \item generator
+
+        n を取り、1からnまでの整数のリストを返す
+
+    \item numberFilter
+
+        整数のリストを取り、特定の性質を持つ数のみを残す。
+        バージョン1では素数の数のみを残す。
+
+    \item count
+
+        整数のリストを取り、その個数を数える。
+
+\end{itemize}
 
 
+次に、numberCount プログラムを変更する。
+変更点は numberFilter 関数の抽出条件とし、素数判定による抽出から偶数判定による抽出とする。
+変更した結果をリストに示す。
+なお、変更部分は下線の部分である。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:numberCountV2,
+                     caption= numberCount プログラムバージョン2,
+                     basicstyle={\small}] {src/numberCount2.hs}
+\end{table}
+
+numberCount プログラムとその変更を Delta Monad によって記述する(リスト\ref{src:numberCountDelta})。
+Delta Monad によって変更を記述したプログラムは全ての値が Delta 型であり、全ての関数はDelta型の値を返す。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:numberCountDelta, caption= Delta を用いて記述した numberCount プログラム,
+                     basicstyle={\footnotesize}] {src/numberCountDelta.hs}
+\end{table}
+
+generator 関数と count 関数は変更が無いために Mono のままである。
+変更された numberFilter 関数は、返り値の Delta のバージョンを2つにしている。
+
+Delta によって表現された numberCount プログラムを実行することで、2つのバージョンを同時に実行することができる。
+実行した結果がリスト\ref{src:numberCountResult}である。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:numberCountResult, caption= Delta によって表現されたnumberCountの実行例] {src/numberCountResult.txt}
+\end{table}
+
+numberCount プログラムに対して 1000 を与えると、1 から 1000 までの中から素数の個数を数えた 168 と、偶数の個数を数えた1000が得られる。
+このように Delta Monad によってプログラムの変更を表すことで全てのバージョンを同時に実行することが可能となる。
+なお、 Delta が Monadであることを保証するMonad則を満たすることは証明支援言語Agdaによって証明した。
+
 \section{他の Monad との組み合せ}
+Delta Monad によりプログラムの変更を表現することができた。
+ここで Delta Monad と他の Monad の組み合せを考える。
+プログラミング言語 Haskell において、入出力は Monad を介して行なわれる。
+よって入出力を行なうプログラムでは Monad を用いるため、 Delta Monad は他の Monad と組み合せが必須となる。
+加えて、Monad により提供される例外やロギングといったメタ計算を組み合せで Delta に組込めるというメリットもある。
+
+Delta Monad と他の Monad を組み合せるためにデータ型 DeltaM を定義した。
+データ型 DeltaM は内部にある Monad のメタ計算と同時にDelta Monad のメタ計算を行なう。
+例えば、DeltaM と Writer Monad を組み合せることにより、実行中の値のログ付きで全バージョン実行を行なうことができる。
+DeltaM も Monad 則を満たすことは Agda によって証明した。
 
 \section{まとめと課題}
-
-\thispagestyle{fancy}
-\begin{thebibliography}{9}
+Delta Monad を用いてプログラムの変更を定義することができた。
+TODO...
 
-\bibitem{1}
+\nocite{Girard:1989:PT:64805, opac-b1092711, BarrM:cattcs, JonesDuponcheel93}
+\thispagestyle{fancy}
 
-\end{thebibliography}
+\bibliographystyle{jplain}
+\bibliography{reference}
+
 \end{document}
--- a/prepaper/Makefile	Tue Feb 17 10:09:22 2015 +0900
+++ b/prepaper/Makefile	Tue Feb 17 12:08:10 2015 +0900
@@ -7,6 +7,7 @@
 
 $(TARGET).dvi : $(wildcard **/*.tex) $(TARGET).tex
 	platex $(TARGET).tex
+	pbibtex $(TARGET)
 	platex $(TARGET).tex
 	platex $(TARGET).tex
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/reference.bib	Tue Feb 17 12:08:10 2015 +0900
@@ -0,0 +1,61 @@
+@book{Girard:1989:PT:64805,
+ author    = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
+ title     = {Proofs and Types},
+ year      = {1989},
+ isbn      = {0-521-37181-3},
+ publisher = {Cambridge University Press},
+ address   = {New York, NY, USA},
+}
+
+@book{opac-b1092711,
+   title     = "Introduction to higher order categorical logic",
+   author    = "Lambek, Joachim (mathématicien) and Scott, P. J.",
+   series    = "Cambridge studies in advanced mathematics",
+   publisher = "Cambridge University Press",
+   address   = "Cambridge, New York (N. Y.), Melbourne",
+   url       = "http://opac.inria.fr/record=b1092711",
+   isbn      = "0-521-24665-2",
+   year      = 1986
+}
+
+@book{BarrM:cattcs,
+    author    = {Barr, Michael and Wells, Charles},
+    title     = {Category Theory for Computing Science},
+    publisher = {Prentice-Hall},
+    series    = {International Series in Computer Science},
+    year      = 1990,
+    note      = {Second edition, 1995},
+    isbn      = {0-13-120486-6},
+    lccn      = {QA76.9.M35B37 1990}
+}
+
+@article{Moggi:1991:NCM:116981.116984,
+    author     = {Moggi, Eugenio},
+    title      = {Notions of Computation and Monads},
+    journal    = {Inf. Comput.},
+    issue_date = {July 1991},
+    volume     = {93},
+    number     = {1},
+    month      = jul,
+    year       = {1991},
+    issn       = {0890-5401},
+    pages      = {55--92},
+    numpages   = {38},
+    url        = {http://dx.doi.org/10.1016/0890-5401(91)90052-4},
+    doi        = {10.1016/0890-5401(91)90052-4},
+    acmid      = {116984},
+    publisher  = {Academic Press, Inc.},
+    address    = {Duluth, MN, USA},
+}
+
+@techreport{JonesDuponcheel93,
+  author      = {M. P. Jones and L. Duponcheel},
+  title       = {Composing monads},
+  institution = {Yale University},
+  year        = {1993},
+  month       = {December},
+  number      = {YALEU/DCS/RR-1004},
+  type        = {Research Report},
+  ftp         = {ftp://ftp.cs.nott.ac.uk/nott-fp/reports/yale/RR-1004.ps}
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/DeltaM.hs	Tue Feb 17 12:08:10 2015 +0900
@@ -0,0 +1,20 @@
+data DeltaM m a = DeltaM (Delta (m a)) deriving (Show)
+
+
+unDeltaM :: DeltaM m a -> Delta (m a)
+unDeltaM (DeltaM d) = d
+
+headDeltaM :: DeltaM m a -> m a
+headDeltaM (DeltaM d) = headDelta d
+
+tailDeltaM :: DeltaM m a -> DeltaM m a
+tailDeltaM (DeltaM d) = DeltaM $ tailDelta d
+
+mu' :: (Functor m, Monad m) => DeltaM m (DeltaM m a) -> DeltaM m a
+mu' d@(DeltaM (Mono _))    = DeltaM $ Mono $ (>>= id) $ fmap headDeltaM $ headDeltaM d
+mu' d@(DeltaM (Delta _ _)) = DeltaM $ Delta ((>>= id) $ fmap headDeltaM $ headDeltaM d)
+                                            (unDeltaM (mu' (fmap tailDeltaM (tailDeltaM d))))
+
+instance (Functor m, Monad m) => Monad (DeltaM m) where
+    return x = DeltaM $ Mono $ return x
+    d >>= f  = mu' $ fmap f d
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/delta_data.hs	Tue Feb 17 12:08:10 2015 +0900
@@ -0,0 +1,1 @@
+data Delta a = Mono a | Delta a (Delta a)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/delta_instance_monad.hs	Tue Feb 17 12:08:10 2015 +0900
@@ -0,0 +1,13 @@
+headDelta :: Delta a -> a
+headDelta (Mono  x)   = x
+headDelta (Delta x _) = x
+
+tailDelta :: Delta a -> Delta a
+tailDelta (Mono x)     = Mono x
+tailDelta (Delta _ ds) = ds
+
+instance Monad Delta where
+ return x = Mono x
+ (Mono x) >>= f    = f x
+ (Delta x d) >>= f = Delta (headDelta (f x))
+                       (d >>= (tailDelta . f))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/numberCount1.hs	Tue Feb 17 12:08:10 2015 +0900
@@ -0,0 +1,5 @@
+generator x     = [1..x]
+numberFilter xs = filter isPrime xs
+count xs        = length xs
+
+numberCount x = count (numberFilter (generator x))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/numberCount2.hs	Tue Feb 17 12:08:10 2015 +0900
@@ -0,0 +1,5 @@
+generator x     = [1..x]
+numberFilter xs = filter @ {\underline {even}} @ xs
+count xs        = length xs
+
+numberCount x = count (numberFilter (generator x))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/numberCountDelta.hs	Tue Feb 17 12:08:10 2015 +0900
@@ -0,0 +1,8 @@
+generator x = Mono [1..x]
+numberFilter xs = let primeList = filter isPrime xs
+                      evenList  = filter even xs    in
+                  Delta evenList (Mono primeList)
+count xs = return (length xs)
+
+numberCount x = count =<< numberFilter =<< generator x
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prepaper/src/numberCountResult.txt	Tue Feb 17 12:08:10 2015 +0900
@@ -0,0 +1,2 @@
+*Main> numberCount 1000
+Delta 500 (Mono 168)