--- a/delta.tex	Thu Feb 12 11:28:50 2015 +0900
+++ b/delta.tex	Thu Feb 12 12:39:57 2015 +0900
@@ -2,26 +2,65 @@
 \label{chapter:delta}
 
 本研究では Monad によりプログラムの変更を定義する。
+第\ref{chapter:delta}章ではプログラムの変更が Monad として表現可能であることを示す。
 
-そのためにまずはプログラムを定義する。
+% {{{ Delta Monad の定義
+
+\section{Delta Monad の定義}
+
+まずはプログラムを定義する。
 プログラムは型付けされた値と、値を値へと写像する関数のみで構成されるものとする。
 プログラムの実行は関数の値への適用とする。
 入出力といった、値や関数で表現できない計算はメタ計算とする。
 メタ計算をある性質を持つデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。
 メタ計算とデータ構造の対応に用いる性質が Monad である。
 
-プログラムの変更とは関数や値が変更されることであり、変更される量には単位があるとする。
-最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。
+例えば、失敗する可能性があるメタ計算 T は式\ref{exp:partiality}のように定義できる。
+
+\begin{equation}
+    T A = A_{ \bot } (i.e. A + \left\{ \bot \right\})
+    \label{exp:partiality}
+\end{equation}
+
+型 A の値に対応するメタ計算 T は、A と $ \bot $ の論理和として表現できる。
+成功した際は A を返し、失敗した場合は $ \bot $ を返す。
+
+ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させるとする。
+プログラムは型付けされた値と、関数の組み合せで構成される。
+例えば、型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。
+
+\begin{equation}
+    g ( f ( x ))
+    \label{exp:non_failure_program}
+\end{equation}
 
-ここで、プログラムが変更される際に過去のバージョンのプログラムも保存するメタ計算を提案する。
-全ての変更単位で変更されたプログラムを保存し、それらを比較することでプログラムの変更を表現しようと考えた。
-このメタ計算を表す Monad を Delta Monad と呼ぶ。
+ここで関数f は失敗する可能性があるとする。
+その時、f が失敗した場合の計算を考える必要がある。
+計算の実現方法はいくつか存在する。
+計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で行なうことで実現できる。
+
+実現方法の1つとして、 Monad を用いたメタ計算がある。
+Monad により失敗した際の計算をメタ計算としてデータ構造に紐付ける。
+式\ref{exp:partiality} で定義したように、計算の成功は型 A 値を返し、失敗は $ \bot $ を返す。
+計算に失敗した際に対応するメタ計算を定義し、関数をそのメタ計算で拡張することで失敗に対する処理が実現できる。
+例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することが実現できる。
+
+型A を持つx の値をメタ計算と対応して型 T A とした値を x' 、メタ計算による関数の拡張を * と記述すると、式\ref{exp:non_failure_program} の式は式\ref{exp:failure_program} のように書ける。
 
-% {{{ Delta Monad の定義
+\begin{equation}
+    {g*} ( {f*} ( x' ))
+    \label{exp:failure_program}
+\end{equation}
 
-\section{Delta Monad の定義}
+ここで重要な点は、元の関数 $ f $ と $g$ から $f*$ と $g*$ が導けることである。
+メタ計算が無い関数 $ f $ とメタ計算を持つ関数 $ f * $ が1対1に対応することは Monad により保証されている。
+このように、値と関数で表されたプログラムにおいてメタ計算を用いることで、計算を拡張することができる。
 
-任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義される。
+プログラムの変更をメタ計算として記述することを考える。
+
+ここで、プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。
+最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。
+任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義する。
 
 \begin{equation}
     T A = V A
@@ -30,6 +69,10 @@
 
 V はプログラムの全てバージョンの集合であり、V AとすることでAに対応する値の集合を返すものとする。
 
+ここで、プログラムが変更される際に過去のバージョンのプログラムも保存するメタ計算を提案する。
+全ての変更単位で変更されたプログラムを保存し、それらを比較することでプログラムの変更を表現しようと考えた。
+このメタ計算を表す Monad を Delta Monad と呼ぶ。
+
 % }}}
 
 % {{{ Haskell における Delta Monad の実装例
@@ -163,3 +206,5 @@
 \end{figure}
 
 % }}}
+
+\section{プログラムの変更に対するメタ計算の例}

--- a/introduction.tex	Thu Feb 12 11:28:50 2015 +0900
+++ b/introduction.tex	Thu Feb 12 12:39:57 2015 +0900
@@ -1,13 +1,17 @@
-\chapter{研究目的}
+\chapter{プログラムの変更の形式化}
 \label{chapter:introduction}
 
 本研究ではプログラムの信頼性の向上を目標とする。
 
 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。
-例えば仕様が未定義の挙動によってプログラムが停止することや、プログラムに記述した誤った条件式よる異なる計算結果、実行環境やパラメタの変化に対応できずに正しくない動作が引き起されることなどがある。
-信頼性を低下させる原因が増えるタイミングの多くはプログラムを変更した時であると考えた。
+例えば仕様が未定義の挙動によってプログラムが停止したり、プログラム内の誤った条件式により計算結果が仕様と異なったり、実行環境やパラメタが変化した際に望まない動作が発生することなどがある。
+信頼性を低下させる原因が増えるタイミングの多くはプログラムを変更した時である。
+よって、プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。
 
 本研究ではプログラムの変更を Monad を用いて形式化する。
-プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。
-信頼性を保ちながら開発するための手法や、変更を形式的に行なうことによって可能となる信頼性の解析などを提案する。
-また、形式化した論理の観点からプログラムの変更が持つ性質などを解析し、ソフトウェア開発手法の指針を提案する。
+プログラムにおけるMonad とはデータ構造とメタ計算の対応である。
+メタ計算とは計算を実現するための計算であり、プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行することができる。
+例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を考える。
+もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと判定できる。
+このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発するための手法を提案する。
+加えて、形式化した論理の観点からプログラムの変更が持つ性質などを解析し、ソフトウェア開発手法の指針を提案する。