Mercurial > hg > Papers > 2015 > atton-thesis
diff delta.tex @ 57:5f0e13923cfd
Fixes
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 16 Feb 2015 16:24:42 +0900 |
parents | 37a832dff044 |
children |
line wrap: on
line diff
--- a/delta.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/delta.tex Mon Feb 16 16:24:42 2015 +0900 @@ -10,10 +10,10 @@ \section{Delta Monad の定義} まずはプログラムを定義する。 -プログラムは型付けされた値と、値を値へと写像する関数のみで構成されるものとする。 +プログラムは型付けされた値と、値を値へと写像する関数のみで構成される。 プログラムの実行は関数の値への適用とする。 -入出力といった、値や関数で表現できない計算はメタ計算とする。 -メタ計算をある性質を持つデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。 +入出力といった、値や関数のみで表現できない計算はメタ計算とする。 +メタ計算を特定のデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。 メタ計算とデータ構造の対応に用いる性質が Monad である。 例えば、失敗する可能性があるメタ計算 T は式\ref{exp:partiality}のように定義できる。 @@ -24,11 +24,10 @@ \end{equation} 型 A の値に対応するメタ計算 T は、A と $ \bot $ の論理和として表現できる。 -成功した際は A を返し、失敗した場合は $ \bot $ を返す。 +計算に成功した際は A を返し、失敗した場合は $ \bot $ を返す。 -ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させるとする。 -プログラムは型付けされた値と、関数の組み合せで構成される。 -例えば、型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。 +ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させる。 +プログラムは型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。 \begin{equation} g ( f ( x )) @@ -37,14 +36,14 @@ ここで関数f は失敗する可能性があるとする。 その時、f が失敗した場合の計算を考える必要がある。 -計算の実現方法はいくつか存在する。 -計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で行なうことで実現できる。 +この計算の実現方法はいくつか存在する。 +計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で判断するなどがある。 実現方法の1つとして、 Monad を用いたメタ計算がある。 Monad により失敗した際の計算をメタ計算としてデータ構造に紐付ける。 式\ref{exp:partiality} で定義したように、計算の成功は型 A 値を返し、失敗は $ \bot $ を返す。 計算に失敗した際に対応するメタ計算を定義し、関数をそのメタ計算で拡張することで失敗に対する処理が実現できる。 -例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することが実現できる。 +例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することができる。 型A を持つx の値をメタ計算と対応して型 T A とした値を x' 、メタ計算による関数の拡張を * と記述すると、式\ref{exp:non_failure_program} の式は式\ref{exp:failure_program} のように書ける。 @@ -57,22 +56,21 @@ メタ計算が無い関数 $ f $ とメタ計算を持つ関数 $ f^{*} $ が1対1に対応することは Monad により保証されている。 このように、値と関数で表されたプログラムにおいてメタ計算を用いることで、計算を拡張することができる。 -プログラムの変更をメタ計算として記述することを考える。 +プログラムとメタ計算の関係としての Monad について述べたところで、プログラムの変更をメタ計算として記述することを考える。 -ここで、プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。 +プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。 最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。 任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義する。 \begin{equation} - T A = V A + T A = V_A \label{exp:meta_computation_definition} \end{equation} -V はプログラムの全てバージョンの集合であり、V AとすることでAに対応する値の集合を返すものとする。 +V はプログラムの全てバージョンの集合であり、$ V_A $ とすることでAに対応する値の集合を返すものとする。 -ここで、プログラムが変更される際に過去のバージョンのプログラムも保存するメタ計算を提案する。 -全ての変更単位で変更されたプログラムを保存し、それらを比較することでプログラムの変更を表現しようと考えた。 -このメタ計算を表す Monad を Delta Monad と呼ぶ。 +式\ref{exp:meta_computation_definition}のメタ計算として、全ての変更単位で変更されたプログラムを保存する計算を提案する。 +このメタ計算を Delta Monad と呼ぶ。 なお、この Delta Monadが Monad であることの証明は \ref{chapter:proof_delta} 章で行なう % }}} @@ -116,7 +114,7 @@ 関数 return は任意の型aを受けとり、メタ計算と対応された型に対応させて返す。 \verb/>>=/ は中置関数であり、left operand と right operand を取る。 -left operand であるメタ計算と対応された値と、right operand であるメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。 +left operand にメタ計算と対応された値と、right operand にメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。 データ型 Delta に対応するメタ計算を Monad を用いてリスト\ref{src:delta_instance_monad}のように定義する。 @@ -133,7 +131,9 @@ \item 中置関数 \verb/>>=/ - メタ計算を含んだ関数の適用であるため、値と関数の同じバージョンを計算して返すものとなる。 + メタ計算を含んだ関数の適用である。 + 通常の関数の適用に加え、バージョンを含んだ計算も行なう。 + 値と関数のそれぞれにおいて同じバージョン選択し、関数を適用する。 もしバージョン1であった場合はコンストラクタは Mono であるため、Mono が持っている値に対して関数を適用することとなる。 もしバージョンが1で無い場合のコンストラクタは Delta であるため、先頭の値を用いて計算し、残りの値と結合することとなる。 その際、先頭の値を取り出すために headDelta 関数を、先頭以外の値を取り出すために tailDelta 関数を用いる。 @@ -194,7 +194,7 @@ Haskell において実装した Delta Monad はプログラムの変更を含めた計算もメタ計算としてHaskellで実行する。 これはプログラムの変更からどのような処理を導くかをメタ計算として Haskell で実行可能であることを意味する。 つまり、図\ref{fig:non_delta_example}のようにプログラムにおいてバージョンが変わるごとにバージョン間の関係が存在しない状態から、図\ref{fig:delta_example}のようにプログラムの変更を含めてプログラムを実行可能となったことを意味する。 -例えば、プログラムの実行時にバージョン間の挙動の比較することで過去の挙動との差異を指摘することなどが可能となる。 +メタ計算を変更することでプログラムの実行時にバージョン間の挙動の比較することも可能となる。 \begin{figure}[htbp] \begin{center} @@ -223,7 +223,7 @@ まず最初に挙げられるものがプログラムの変更を保存するメタ計算である。 これは Delta Monad として実際に定義できた。 -プログラムの変更を保存した場合、以下のような方法により信頼性の向上が見込めると考える。 +プログラムの変更を保存した場合、以下のような計算可能となる。 \begin{itemize} @@ -231,10 +231,10 @@ プログラムの変更列から任意のバージョン2つを取り出し、同時に実行するプログラムを構成する。 プログラムを同時に実行することで以下のようなメリットがある。 - なお、任意の要素の組み合せは category において product として表現されるため、 product と対応があると考えている。 + なお、任意の要素どうしの組み合せは category において product として表現されるため、 product と対応があると考えている。 \begin{itemize} - \item 実行系とサブの実行系を実行することができる。 + \item 実行系とサブの実行系を実行する 例えば、あるバージョンでリリースしたプログラムがあるとする。 変更を加え、ベータ版としてリリースしたいが動作が不安定である。 @@ -245,7 +245,7 @@ 異なるバージョン間でプロトコルに互換が無いプログラムを考える。 バージョン間の互換を含めてメタ計算として定義し、全てのバージョンに対して互換を持つプログラムを構築する。 - そうすることによりどのバージョンのプロトコルとも互換を持つような変換器を作成できる。 + そうすることで、どのバージョンのプロトコルとも互換を持つような変換器を作成できる。 \end{itemize} @@ -258,8 +258,8 @@ \begin{itemize} \item 過去のバージョンの挙動を破壊する時を検出する - プログラムの変更の際、トレースを変えてはいけない部分が存在するとする。 - 変更の際にトレースが変更したことを検出することにより、トレースが保存される変更のみを受けつけるようにする。 + プログラムの変更の際、トレースを変えてはいけない部分を指定する。 + 変更の際にトレースが保存される変更のみを受けつけるようにする。 \item トレースが変化していないことを確認する @@ -284,8 +284,8 @@ \end{itemize} 他にもプログラムの変更そのものを処理するプログラムを定義することもできる。 -この機構を言語処理系に組込むことにより、プログラムの変更方法も言語の仕様に含めることができる。 -例えば、プログラムの変更は許可されたオペレーション内で行なうといった制約を含めることが可能となる。 +この機構を言語処理系に組込むことにより、言語の仕様にプログラムの変更方法も含めることができる。 +例えば、プログラムの変更は許可されたオペレーション内で行なうといった制約を加えることが可能となる。 さらにユーザによりプログラムの変更に対するメタ計算を自由に定義できるような言語処理系を作るとする。 その処理系ではこれまでに挙げた全てのメタ計算の例から使いたい機能を選んだり自分で追加することが可能となる。