Mercurial > hg > Papers > 2015 > atton-midterm

annotate bachelor_middle_draft.tex @ 3:331d9984930f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes from hiyoko-san check
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 29 Oct 2014 12:30:55 +0900
parents 514bb884084c
children 0805d4984b1f
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 \usepackage[dvips]{graphicx}
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
3 \usepackage{cprotect}
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 \usepackage{picins}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 \usepackage{fancyhdr}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 \usepackage{eclbkbox}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 \usepackage{url}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 %\pagestyle{fancy}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 \rhead{}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 \cfoot{}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 \setlength{\headheight}{0mm}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 \setlength{\headsep}{5mm}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 \setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 \setlength{\textwidth}{181mm}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 \setlength{\textheight}{261mm}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 \setlength{\footskip}{0mm}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 \pagestyle{empty}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 \begin{document}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 \title{Modify Program by Monad}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 \author{115763K 氏名 {比嘉}{健太} 指導教員 : 河野真治}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 \date{}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 \maketitle
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 \thispagestyle{fancy}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
30 % {{{ プログラムの変更を表すMonad
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
32 \section{プログラムの変更を表すMonad}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
33 プログラムを変更するとプログラムの実行結果も変化する。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
34 しかし、変更後のプログラムが正しい実行結果でない場合も存在する。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
35 そこで、プログラムに対する変更をMonadとして記述する。
3
331d9984930f Fixes from hiyoko-san check
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
36 Monadとして変更を記述することで、プログラムの変更時にこのプログラムの変更が正しく完成に近づくような変更なのか評価する。
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
37 ひいては、プログラムを変更することの意味や性質などを解析する。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 % }}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
41 % {{{ 限定されたプログラムの変更を表す Delta Monad
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
43 \section{限定されたプログラムの変更を表す Delta Monad}
3
331d9984930f Fixes from hiyoko-san check
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
44 Monad を用いたプログラムの変更の例として、プログラミング言語HaskellにおけるMonadを利用する。
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
45 Haskell におけるMonadとはメタ計算と対応されたデータ型である。
3
331d9984930f Fixes from hiyoko-san check
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
46 Monadであるデータ型は任意の型を内包することができ、内包した型に対する計算を行なった際にメタ計算も同時に行なう。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
48 Haskell において限定されたプログラムの変更を表すことができる Delta Monad を定義した。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
49 Delta Monad におけるプログラムの変更は、変更前と変更後の実行結果を両方持つことによって表現する。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
50 また、実行結果に対する変更履歴を持ち、2つ変更履歴の比較によってプログラムがどのように変更したか判断する。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
51
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
52 データ型Delta の定義を示す(図\ref{delta-monad-definition})。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
54 % {{{ Definiton Delta
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
55
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
56 \begin{breakbox}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
57 \verb/ data Delta a = Delta [String] a [String] a/
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
58 \caption{型変数を持つ型 Delta の定義(Haskell)}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
59 \label{delta-monad-definition}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
60 \end{breakbox}
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 % }}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
64 データ型 Delta は任意の型aの変数を持つことができる。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
65 型aの変数を2つと変数に対する実行履歴となる文字列のリストを2つ持つ。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
66 このデータ型をMonadとして利用するが、あるデータ型をMonadとするためには関数 return と \verb/>>=/ を定義する必要がある(図\ref{monad-class})。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
68 % {{{ Definiton Delta
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 \begin{breakbox}
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
71 \begin{verbatim}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
72 return :: Monad m => a -> m a
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
73 (>>=) :: Monad m => m a -> (a -> m b) -> m b
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
74 \end{verbatim}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
75 \caption{データ型をMonadとするために必要な関数}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
76 \label{monad-class}
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 \end{breakbox}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 % }}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
81 図\ref{monad-class} の定義は関数の型のみ記述している。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
82 m は Monad であり、m a は任意の型 a を内包するMonadである。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
83 return は任意の型aからm aの値を返す関数 return がある。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
84 return は任意の型の値をMonadに内包するために利用する。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
85 中置関数\verb/(>>=)/ はMonadの値 m a と、aを取って m b を返す関数を取り、m b の値を返す。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
86 \verb/(>>=)/の定義がMonadに対するメタ計算の定義となる。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
88 Delta におけるreturnと\verb/>>=/の定義を図\ref{monad-instance-delta}に示す。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
90 % {{{ instance Monad Delta
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 \begin{breakbox}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 \begin{verbatim}
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
94 mu (Delta lx (Delta llx x _ _)
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
95 ly (Delta _ _ lly y)) =
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
96 Delta (lx ++ llx) x (ly ++ lly) y
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
98 instance Monad Delta where
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
99 return x = Delta [] x [] x
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 d >>= f = mu $ fmap f d
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 \end{verbatim}
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
102 \cprotect\caption{Delta に対する return と\verb/(>>=)/ の定義}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
103 \label{monad-instance-delta}
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 \end{breakbox}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 % }}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
108 return においては実行履歴が存在しない空の文字列を含んだMonadを返す。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
109 型a の値xは2つに分解され、異なる実行結果を得るために利用する。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
110 \verb/(>>=)/においては、異なる実行結果に対して対応する実行履歴を保存しながら関数を適用する。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
112 これらの関数returnと\verb/>>=/は満たすべきMonad則が存在する。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
113 型Deltaに対するこれらの関数がMonad則を満たしていることは定理証明支援系プログラミング言語Agda\cite{agda}によって証明した。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 % }}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
117
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
118 % {{{ Delta Monad におけるプログラムの変更例
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
120 \section{Delta Monad におけるプログラムの変更例}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
121 Delta Monad を用いたHaskellのプログラムを示す(図\ref{delta-program})。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
123 % {{{ delta.hs
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 \begin{breakbox}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 {\scriptsize
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 \begin{verbatim}
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
128 generator :: Int -> Delta [Int]
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 generator x = let intList = [1..x] in
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 returnD intList
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
132 primeFilter :: [Int] -> Delta [Int]
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 primeFilter xs = let primeList = filter isPrime xs
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 refactorList = filter even xs in
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 returnDD primeList refactorList
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
137 count :: [Int] -> Delta Int
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138 count xs = let primeCount = length xs in
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 returnD primeCount
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
141 primeCount :: Int -> Delta Int
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 primeCount x = generator x >>= primeFilter >>= count
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 \end{verbatim}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 }
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
145 \caption{Delta Monadを用いたプログラムの例}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
146 \label{delta-program}
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 \end{breakbox}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 % }}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 このプログラムは整数nを取り、1からnまでの整数の中から素数の個数を調べるプログラムである。
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 1からnまでの整数の個数を調べるprimeCount 関数は3つの関数からなる
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 \begin{itemize}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 \item 1 から n までの整数を返す関数 generator
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 \item 整数のリストから素数であるもののみを残したリストを返す関数 primeFilter
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 \item リストの中に存在する要素の個数を返す関数 count
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 \end{itemize}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
160 このプログラムの primeFilter 関数が返す Delta Monad を変更する。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 本来ならば素数である整数のみを返す計算だったが、変更により偶数である整数のみを返すようにした。
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
162 図\ref{delta-program}のプログラムを実行した例が図\ref{delta-result}である。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 % {{{ results
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 \begin{breakbox}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167 {\small
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168 \begin{verbatim}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 *Main> primeCount 10
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
170 Delta
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
171 ["[1,2,3,4,5,6,7,8,9,10]","[2,3,5,7]","4"] 4
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
172 ["[1,2,3,4,5,6,7,8,9,10]","[2,4,6,8,10]","5"] 5
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 \end{verbatim}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 }
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
175 \caption{Delta Monad を用いたプログラムの実行例}
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
176 \label{delta-result}
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 \end{breakbox}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 % }}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181 変更前のプログラムの実行順序が上側の実行結果である。
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 \begin{itemize}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 \item 1 から 10 までのリストを作成し
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
184 \item 素数のみを残すために 2,3,5,7 が残り
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
185 \item その個数を数えるために4となる
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
186 \end{itemize}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
187 変更後のプログラムの実行順序が下側の実行結果である。
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
188 \begin{itemize}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
189 \item 1 から 10 までのリストを作成し
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
190 \item 偶数のみを残すために 2,4,6,8,10 が残り
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
191 \item その個数を数えるために5となる
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
192 \end{itemize}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
193
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
194 変更前の実行結果を保存しながら、プログラムが変更された後の新しい実行結果が得られた。
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
195 この実行結果を比較することにより、変更前のプログラムの実行結果が損なわれていないか検知する。
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
196
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
197 今回は検証のために変更前と変更後の両方のプログラムを実行した。
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
198 しかし、必ず両方実行しなくてはならない訳では無い。
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
199 Haskell には遅延評価の機構が備わっており、値は必要とされるまで計算が実行されない。
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
200 そのため、変更後のプログラムの実行結果のみを表示する場合などは変更前の計算は行なわれない。
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
201 遅延評価とDelta Monadを組み合わせることで、必要の無い計算は増やさずに変更前のプログラムを保存できる。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
202
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
203 % }}}
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
204
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
205 % {{{ まとめと課題
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
206
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
207 \section{まとめと課題}
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
208 Delta Monad を定義することにより、変更前のプログラムを保存しつつ変更後のプログラムとしても実行することが可能となった。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
209 さらに、実行履歴が得られるためプログラムがどのように変化したかを確認することもできる。
1
9d656911de30 Comment from kono-lab-members
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
210
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
211 今回定義したDelta Monad はプログラムの変更を保持できるのは1つのMonadにつき2つまでという制約がある。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
212 Delta Monad を拡張し、無限個の変更を扱えるようにすることでプログラムの変更をMonadのみで記述する。
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
213 Monad のみでプログラムの変更を記述することにより、Monadの理論的背景である圏論の視点からプログラムを変更することの意味論を探る。
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
214
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
215 % }}}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
216
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
217 \begin{thebibliography}{9}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
218
2
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
219 \bibitem{moggi} Eugenio Moggi, Notion of Computation and Monads(1991)
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
220 \bibitem{proofs-and-types} Jean-Yves Girard, Paulr Taylor, Yves Lafont, Proofs and Types(1990)
514bb884084c Update v2.0
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
221 \bibitem{agda} The Agda Wiki - Agda \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}
0
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
222
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
223 \end{thebibliography}
95a86a261203 Migrate from atton/texts/bachelor_middle_draft
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
224 \end{document}