Mercurial > hg > Papers > 2015 > atton-thesis

annotate delta.tex @ 25:a0d91fbf4876

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add description prove method in agda
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 10 Feb 2015 12:48:02 +0900
parents 43d3e7b31fc0
children 67d79c18a276
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{プログラムの変更を表現する Delta Monad}
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
2 \label{chapter:delta}
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 本研究では Monad によりプログラムの変更を定義する。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 そのためにまずはプログラムを定義する。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 プログラムは型付けされた値と、値を値へと写像する関数のみで構成されるものとする。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 プログラムの実行は関数の値への適用とする。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 入出力といった、値や関数で表現できない計算はメタ計算とする。
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
10 メタ計算をある性質を持つデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 メタ計算とデータ構造の対応に用いる性質が Monad である。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 プログラムの変更とは関数や値が変更されることであり、変更される量には単位があるとする。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 ここで、プログラムが変更される際に過去のバージョンのプログラムも保存するメタ計算を提案する。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 全ての変更単位で変更されたプログラムを保存し、それらを比較することでプログラムの変更を表現しようと考えた。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 このメタ計算を表す Monad を Delta Monad と呼ぶ。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
20 % {{{ Delta Monad の定義
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
21
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 \section{Delta Monad の定義}
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
24 任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義される。
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 \begin{equation}
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 T A = V A
11
76ce5bb18092 Add Category definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 10
diff changeset
28 \label{exp:meta_computation_definition}
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 \end{equation}
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 V はプログラムの全てバージョンの集合であり、V AとすることでAに対応する値の集合を返すものとする。
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
33 % }}}
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
34
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
35 % {{{ Haskell における Delta Monad の実装例
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
36
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 \section{Haskell における Delta Monad の実装例}
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
12
11015b94a5cd Add figures category
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
39 式\ref{exp:meta_computation_definition}のメタ計算をMonadで実現する。
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 実装例としてプログラミング言語 Haskell を用いる。
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
42
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
43 まずは全てのプログラムのバージョンを表わすデータ型 Delta を考える。
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
44 Delta の定義はリスト\ref{src:delta_constructor} とする。
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
45
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
46 \begin{table}[html]
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
47 \lstinputlisting[label=src:delta_constructor, caption=Haskellにおけるデータ型Deltaの定義]{src/delta_constructor.hs}
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
48 \end{table}
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
49
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
50 データ型 Delta はコンストラクタ Delta もしくは Mono によって構成される。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
51 バージョンが1である値は Mono によって構成される。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
52 プログラムを変更する際には、コンストラクタ Delta を用いて記述し、変更後の値と前のバージョンを持つ。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
53 なお、a とは任意の型であり、Delta が任意の型の値に対してもデータ型を構築できることを示す。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
54
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
55 データ型 Delta に対応するメタ計算はリスト\ref{src:delta_instance_monad}のように定義する。
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
56
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
57 \begin{table}[html]
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
58 \lstinputlisting[label=src:delta_instance_monad, caption=Haskell におけるデータ型Deltaとメタ計算の関連付け]
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
59 {src/delta_instance_monad.hs}
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
60 \end{table}
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
61
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
62 Haskell においてメタ計算とデータ型の対応は Monad によって行なうため、 Monad という型クラスが用意されている。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
63 型クラスとは特定の性質を持つ型をまとめるための制約である。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
64 ある型が型クラスに属するためには制約として型クラスによって指定された関数を定義する必要がある。
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
65 型クラス Monad に要請される関数は return と \verb/>>=/ であり、型クラスはリスト\ref{src:monad_class}のように定義されている。
8
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
66
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
67 \begin{table}[html]
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
68 \lstinputlisting[label=src:monad_class, caption=Haskell における Monad 型クラス]
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
69 {src/monad_class.hs}
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
70 \end{table}
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
71
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
72 関数 return は任意の型aを受けとり、メタ計算と対応された型に対応させて返す。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
73 \verb/>>=/ は中置関数であり、left operand と right operand を取る。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
74 left operand であるメタ計算と対応された値と、right operand であるメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
75
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
76 型クラスMonad を Delta に適用した結果は以下のようになる。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
77
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
78 \begin{itemize}
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
79 \item 関数 return
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
80
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
81 通常の値をメタ計算と対応させるため、値をバージョン1の値とする。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
82 そのためにコンストラクタ Mono を用いる。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
83
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
84 \item 中置関数 \verb/>>=/
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
85
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
86 メタ計算を含んだ関数の適用であるため、値と関数の同じバージョンを計算して返すものとなる。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
87 もしバージョン1であった場合はコンストラクタは Mono であるため、Mono が持っている値に対して関数を適用することとなる。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
88 もしバージョンが1で無い場合のコンストラクタは Delta であるため、先頭の値を用いて計算し、残りの値と結合することとなる。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
89 その際、先頭の値を取り出すために headDelta 関数を、先頭以外の値を取り出すために tailDelta 関数を用いる。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
90 \end{itemize}
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
91
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
92 なお、中置関数 \verb/>>=/ で用いたコンストラクタによる処理の分岐はパターンマッチと呼ばれる。
c4da3e667aad Add Delta definition in Haskell
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
93 Haskell ではコンストラクタごとに関数を記述することでパターンマッチを実現する。
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
95 % }}}
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
96
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
97 % {{{ Delta を用いたプログラムの変更の記述例
6
3b861ecdec9b Add description meta computation
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98
9
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
99 \section{Delta を用いたプログラムの変更の記述例}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
100 プログラムの変更を表現するメタ計算に対応するデータ型 Delta が記述できた。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
101
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
102 実際に Haskell で Delta を用いたプログラムの変更例をリスト\ref{src:delta_example}に示す。
9
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
103
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
104 \begin{table}[html]
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
105 \lstinputlisting[label=src:delta_example, caption=Deltaを用いたプログラムの例]
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
106 {src/delta_example.hs}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
107 \end{table}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
108
19
43d3e7b31fc0 Fix listings and page numbering
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
109 リスト\ref{src:delta_example}は1からnの間の整数に含まれる特定の数の個数を調べるプログラム numberCount である。
9
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
110
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
111 このプログラムは3つの関数からなり、2つのバージョンを含む。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
112
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
113 \begin{itemize}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
114 \item generator
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
115
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
116 1からnの間の整数を生成する関数である。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
117 nを渡すことにより1からnの間の整数のリストを返す。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
118
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
119 \item numberFilter
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
120
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
121 数のリストから特定の数のみを絞り込む関数である。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
122 バージョン1では素数の数のみを絞り込み、バージョン2では偶数の数のみを絞り込んでいる。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
123
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
124 \item count
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
125
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
126 数の個数を数える関数である。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
127 整数はリストで与えられるため、リストの長さが個数であるとした。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
128 \end{itemize}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
129
10
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
130 これらの関数3つをMonad の \verb/>>=/ によってメタ計算を含む関数呼び出しとして実行する。
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
131 3つの関数を実行する関数が numberCount 関数であり、この関数がプログラム本体である。
c2dda6eeab57 Split chapter 3
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
132 numberCount を実行すると \ref{txt:delta_example_result}のような結果が得られる。
9
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
133
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
134 \begin{table}[html]
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
135 \lstinputlisting[label=txt:delta_example_result, caption=numberCountプログラムの実行結果] {src/delta_example_result.txt}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
136 \end{table}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
137
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
138 これはnに1000を与えた結果である。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
139 バージョン1の時は素数の数を求めるため計算結果は168であり、バージョン2の時は偶数の数を求めるために計算結果は500となる。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
140
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
141 3つの関数で構成されたプログラムに対して1つの変更を加えたプログラムを表現することができた。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
142 つまり、Monad によってプログラムの変更をメタ計算として定義できたと言える。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
143
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
144 Haskell において実装した Delta Monad はプログラムの変更を含めた計算もメタ計算としてHaskellで実行する。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
145 これはプログラムの変更からどのような処理を導くかをメタ計算として Haskell で実行可能であることを意味する。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
146 つまり、図\ref{fig:non_delta_example}のようにプログラムにおいてバージョンが変わるごとにバージョン間の関係が存在しない状態から、図\ref{fig:delta_example}のようにプログラムの変更を含めてプログラムを実行可能となったことを意味する。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
147 例えば、プログラムの実行時にバージョン間の挙動の比較することで過去の挙動との差異を指摘することなどが可能となる。
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
148
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
149 \begin{figure}[htbp]
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
150 \begin{center}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
151 \includegraphics[scale=0.8]{fig/non_delta_example.pdf}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
152 \caption{Deltaを用いない通常のプログラムの例}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
153 \label{fig:non_delta_example}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
154 \end{center}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
155 \end{figure}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
156
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
157 \begin{figure}[htbp]
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
158 \begin{center}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
159 \includegraphics[scale=0.8]{fig/delta_example.pdf}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
160 \caption{Deltaを用いたプログラムの例}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
161 \label{fig:delta_example}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
162 \end{center}
324111203070 Add example used delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
163 \end{figure}
14
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
164
586f3ce1effe Add folding for section
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 12
diff changeset
165 % }}}