Papers/2015/atton-thesis: delta.tex annotate

annotate delta.tex @ 30:67d79c18a276

Update description and delta definition

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Thu, 12 Feb 2015 12:39:57 +0900
parents	43d3e7b31fc0
children	d0d14c0a795b

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 によりプログラムの変更を定義する。
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	5 第\ref{chapter:delta}章ではプログラムの変更が Monad として表現可能であることを示す。
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	6
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	7 % {{{ Delta Monad の定義
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	8
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	9 \section{Delta Monad の定義}
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	10
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	11 まずはプログラムを定義する。
6 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 入出力といった、値や関数で表現できない計算はメタ計算とする。
10 c2dda6eeab57 Split chapter 3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	15 メタ計算をある性質を持つデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	16 メタ計算とデータ構造の対応に用いる性質が Monad である。
3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	17
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	18 例えば、失敗する可能性があるメタ計算 T は式\ref{exp:partiality}のように定義できる。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	19
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	20 \begin{equation}
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	21 T A = A_{ \bot } (i.e. A + \left\{ \bot \right\})
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	22 \label{exp:partiality}
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	23 \end{equation}
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	24
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	25 型 A の値に対応するメタ計算 T は、A と $ \bot $ の論理和として表現できる。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	26 成功した際は A を返し、失敗した場合は $ \bot $ を返す。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	27
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	28 ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させるとする。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	29 プログラムは型付けされた値と、関数の組み合せで構成される。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	30 例えば、型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	31
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	32 \begin{equation}
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	33 g ( f ( x ))
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	34 \label{exp:non_failure_program}
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	35 \end{equation}
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	36
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	37 ここで関数f は失敗する可能性があるとする。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	38 その時、f が失敗した場合の計算を考える必要がある。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	39 計算の実現方法はいくつか存在する。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	40 計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で行なうことで実現できる。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	41
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	42 実現方法の1つとして、 Monad を用いたメタ計算がある。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	43 Monad により失敗した際の計算をメタ計算としてデータ構造に紐付ける。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	44 式\ref{exp:partiality} で定義したように、計算の成功は型 A 値を返し、失敗は $ \bot $ を返す。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	45 計算に失敗した際に対応するメタ計算を定義し、関数をそのメタ計算で拡張することで失敗に対する処理が実現できる。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	46 例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することが実現できる。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	47
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	48 型A を持つx の値をメタ計算と対応して型 T A とした値を x' 、メタ計算による関数の拡張を * と記述すると、式\ref{exp:non_failure_program} の式は式\ref{exp:failure_program} のように書ける。
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	49
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	50 \begin{equation}
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	51 {g} ( {f} ( x' ))
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	52 \label{exp:failure_program}
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	53 \end{equation}
14 586f3ce1effe Add folding for section Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	54
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	55 ここで重要な点は、元の関数 $ f $ と $g$ から $f$ と $g$ が導けることである。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	56 メタ計算が無い関数 $ f $ とメタ計算を持つ関数 $ f * $ が1対1に対応することは Monad により保証されている。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	57 このように、値と関数で表されたプログラムにおいてメタ計算を用いることで、計算を拡張することができる。
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	58
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	59 プログラムの変更をメタ計算として記述することを考える。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	60
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	61 ここで、プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	62 最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	63 任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義する。
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	64
3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	65 \begin{equation}
3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	66 T A = V A
11 76ce5bb18092 Add Category definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 10 diff changeset	67 \label{exp:meta_computation_definition}
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	68 \end{equation}
3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	69
3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	70 V はプログラムの全てバージョンの集合であり、V AとすることでAに対応する値の集合を返すものとする。
3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	71
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	72 ここで、プログラムが変更される際に過去のバージョンのプログラムも保存するメタ計算を提案する。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	73 全ての変更単位で変更されたプログラムを保存し、それらを比較することでプログラムの変更を表現しようと考えた。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	74 このメタ計算を表す Monad を Delta Monad と呼ぶ。
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	75
14 586f3ce1effe Add folding for section Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	76 % }}}
8 c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	77
14 586f3ce1effe Add folding for section Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	78 % {{{ Haskell における Delta Monad の実装例
8 c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	79
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	80 \section{Haskell における Delta Monad の実装例}
3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	81
12 11015b94a5cd Add figures category Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 11 diff changeset	82 式\ref{exp:meta_computation_definition}のメタ計算をMonadで実現する。
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	83
3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	84 実装例としてプログラミング言語 Haskell を用いる。
8 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 まずは全てのプログラムのバージョンを表わすデータ型 Delta を考える。
19 43d3e7b31fc0 Fix listings and page numbering Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 14 diff changeset	87 Delta の定義はリスト\ref{src:delta_constructor} とする。
8 c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	88
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	89 \begin{table}[html]
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	90 \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	91 \end{table}
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	92
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	93 データ型 Delta はコンストラクタ Delta もしくは Mono によって構成される。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	94 バージョンが1である値は Mono によって構成される。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	95 プログラムを変更する際には、コンストラクタ Delta を用いて記述し、変更後の値と前のバージョンを持つ。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	96 なお、a とは任意の型であり、Delta が任意の型の値に対してもデータ型を構築できることを示す。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	97
19 43d3e7b31fc0 Fix listings and page numbering Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 14 diff changeset	98 データ型 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	99
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	100 \begin{table}[html]
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	101 \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	102 {src/delta_instance_monad.hs}
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	103 \end{table}
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	104
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	105 Haskell においてメタ計算とデータ型の対応は Monad によって行なうため、 Monad という型クラスが用意されている。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	106 型クラスとは特定の性質を持つ型をまとめるための制約である。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	107 ある型が型クラスに属するためには制約として型クラスによって指定された関数を定義する必要がある。
19 43d3e7b31fc0 Fix listings and page numbering Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 14 diff changeset	108 型クラス 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	109
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	110 \begin{table}[html]
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	111 \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	112 {src/monad_class.hs}
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	113 \end{table}
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	114
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	115 関数 return は任意の型aを受けとり、メタ計算と対応された型に対応させて返す。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	116 \verb/>>=/ は中置関数であり、left operand と right operand を取る。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	117 left operand であるメタ計算と対応された値と、right operand であるメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	118
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	119 型クラスMonad を Delta に適用した結果は以下のようになる。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	120
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	121 \begin{itemize}
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	122 \item 関数 return
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	123
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	124 通常の値をメタ計算と対応させるため、値をバージョン1の値とする。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	125 そのためにコンストラクタ Mono を用いる。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	126
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	127 \item 中置関数 \verb/>>=/
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	128
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	129 メタ計算を含んだ関数の適用であるため、値と関数の同じバージョンを計算して返すものとなる。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	130 もしバージョン1であった場合はコンストラクタは Mono であるため、Mono が持っている値に対して関数を適用することとなる。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	131 もしバージョンが1で無い場合のコンストラクタは Delta であるため、先頭の値を用いて計算し、残りの値と結合することとなる。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	132 その際、先頭の値を取り出すために headDelta 関数を、先頭以外の値を取り出すために tailDelta 関数を用いる。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	133 \end{itemize}
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	134
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	135 なお、中置関数 \verb/>>=/ で用いたコンストラクタによる処理の分岐はパターンマッチと呼ばれる。
c4da3e667aad Add Delta definition in Haskell Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 6 diff changeset	136 Haskell ではコンストラクタごとに関数を記述することでパターンマッチを実現する。
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	137
14 586f3ce1effe Add folding for section Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	138 % }}}
586f3ce1effe Add folding for section Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	139
586f3ce1effe Add folding for section Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	140 % {{{ Delta を用いたプログラムの変更の記述例
6 3b861ecdec9b Add description meta computation Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	141
9 324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	142 \section{Delta を用いたプログラムの変更の記述例}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	143 プログラムの変更を表現するメタ計算に対応するデータ型 Delta が記述できた。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	144
19 43d3e7b31fc0 Fix listings and page numbering Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 14 diff changeset	145 実際に Haskell で Delta を用いたプログラムの変更例をリスト\ref{src:delta_example}に示す。
9 324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	146
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	147 \begin{table}[html]
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	148 \lstinputlisting[label=src:delta_example, caption=Deltaを用いたプログラムの例]
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	149 {src/delta_example.hs}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	150 \end{table}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	151
19 43d3e7b31fc0 Fix listings and page numbering Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 14 diff changeset	152 リスト\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	153
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	154 このプログラムは3つの関数からなり、2つのバージョンを含む。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	155
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	156 \begin{itemize}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	157 \item generator
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	158
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	159 1からnの間の整数を生成する関数である。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	160 nを渡すことにより1からnの間の整数のリストを返す。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	161
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	162 \item numberFilter
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	163
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	164 数のリストから特定の数のみを絞り込む関数である。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	165 バージョン1では素数の数のみを絞り込み、バージョン2では偶数の数のみを絞り込んでいる。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	166
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	167 \item count
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	168
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	169 数の個数を数える関数である。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	170 整数はリストで与えられるため、リストの長さが個数であるとした。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	171 \end{itemize}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	172
10 c2dda6eeab57 Split chapter 3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	173 これらの関数3つをMonad の \verb/>>=/ によってメタ計算を含む関数呼び出しとして実行する。
c2dda6eeab57 Split chapter 3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	174 3つの関数を実行する関数が numberCount 関数であり、この関数がプログラム本体である。
c2dda6eeab57 Split chapter 3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 9 diff changeset	175 numberCount を実行すると \ref{txt:delta_example_result}のような結果が得られる。
9 324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	176
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	177 \begin{table}[html]
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	178 \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	179 \end{table}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	180
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	181 これはnに1000を与えた結果である。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	182 バージョン1の時は素数の数を求めるため計算結果は168であり、バージョン2の時は偶数の数を求めるために計算結果は500となる。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	183
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	184 3つの関数で構成されたプログラムに対して1つの変更を加えたプログラムを表現することができた。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	185 つまり、Monad によってプログラムの変更をメタ計算として定義できたと言える。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	186
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	187 Haskell において実装した Delta Monad はプログラムの変更を含めた計算もメタ計算としてHaskellで実行する。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	188 これはプログラムの変更からどのような処理を導くかをメタ計算として Haskell で実行可能であることを意味する。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	189 つまり、図\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	190 例えば、プログラムの実行時にバージョン間の挙動の比較することで過去の挙動との差異を指摘することなどが可能となる。
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	191
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	192 \begin{figure}[htbp]
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	193 \begin{center}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	194 \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	195 \caption{Deltaを用いない通常のプログラムの例}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	196 \label{fig:non_delta_example}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	197 \end{center}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	198 \end{figure}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	199
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	200 \begin{figure}[htbp]
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	201 \begin{center}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	202 \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	203 \caption{Deltaを用いたプログラムの例}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	204 \label{fig:delta_example}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	205 \end{center}
324111203070 Add example used delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 8 diff changeset	206 \end{figure}
14 586f3ce1effe Add folding for section Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	207
586f3ce1effe Add folding for section Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 12 diff changeset	208 % }}}
30 67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	209
67d79c18a276 Update description and delta definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 19 diff changeset	210 \section{プログラムの変更に対するメタ計算の例}

Mercurial > hg > Papers > 2015 > atton-thesis

annotate delta.tex @ 30:67d79c18a276