--- a/delta.tex	Thu Feb 26 17:57:31 2015 +0900
+++ b/delta.tex	Fri Feb 27 17:07:58 2015 +0900
@@ -72,33 +72,85 @@
 Delta Monad represents modifications by accumulates all versions of a program.
 Accumulated modifications can computes by meta computation.
 In this paper, We propose meta computation execute a program includes modifications simultaneously on Delta.
-Additionally, Delta Monad can be used with other Monads for more computations of modifications.
 
 \section{Programs and Monads}
 Programs notated typed lambda calculus constructed values and abstractions.
 Abstractions maps value to value.
+Abstraction f applies to x notated $ f x $.
 Every lambda term has a type.
 Value x has type A notated $ x : A $.
 Abstraction f has a argument of type A and return value of type B notated $ f : A \rightarrow B $.
 
-\begin{eqnarray}
+\begin{eqnarray*}
     x : A \\
     f : A \rightarrow B \\
-    f x : B
-\end{eqnarray}
+    f x : B \\
+\end{eqnarray*}
+
+Type matched abstractions can be composed by operator ';'.
+Order of composition are commutative.
+
+\begin{eqnarray*}
+    f : A \rightarrow B \\
+    g : B \rightarrow C \\
+    f;g : A \rightarrow C \\
+    \\
+    h : C \rightarrow D \\
+    (f;g);h = f;(g;h)
+\end{eqnarray*}
+
+Abstractions can be extended using Monad.
+
+Monad is $ triple (T, \eta, \mu) $ satisfies laws(Figure) % TODO :commutative diagram
+Various meta computations represents by definition of triple.
+Monad has another description Kleisli Triple $ (T, \eta, \_^{*}) $.
+Kleisli triple are following equations hold:
+
+\begin{itemize}
+    \item $ \eta^{*}_A    = id_{T A} $
+    \item $ \eta;f^{*}    = f \mbox{ for } f : A \rightarrow T B $
+    \item $ f^{*} ; g^{*} = (f; g^{*})^{*} \mbox{ for } f : A \rightarrow T B \mbox{ and } g : B \rightarrow T C $
+\end{itemize}
+
+Kleisli Triple can build from Monad ($ (T, \eta, \mu) $).
+
+For Example, definition of diverging computation using Monad are shown.
 
-Execution of a program is application of abstraction.
-Some computations can not be notated abstraction like Input/Output are meta computation.
-Meta computations are computations for implements computations.
+\begin{itemize}
+    \item $ T A = A_{\bot} (= A + \{\bot\}) $
+    \item $ \eta_A $ is the inclusion of A into $ A_{\bot} $
+    \item if $ f : A \rightarrow T B $, then $ f^{*} (\bot) = \bot $ and $ f^{*}(a) = f (a) $ when $ a $  has type A.
+\end{itemize}
+
+\section{Modification using Monad}
+
+\begin{equation*}
+    T A = A_0 \times A_1 \times \dots \times A_n
+\end{equation*}
+
+\begin{eqnarray*}
+    x : A \\
+    x^{*} : T A \\
+    x^{*} : A_0 \times A_1 \times \dots \times A_n \\
+    \\
+    f : A \rightarrow B \\
+    f^{*} : A \rightarrow T B \\
+    f^{*} : (A_0 \rightarrow B_0) \times (A_1 \rightarrow B_1) \times \dots \times (A_n \rightarrow B_n)
+\end{eqnarray*}
+
+\begin{eqnarray*}
+    f^{*} : A \rightarrow T B \\
+    f^{*} = f_0 \times f_1 \times \dots f_n \\
+    \\
+    g^{*} : B \rightarrow T C \\
+    g^{*} = g_0 \times g_1 \times \dots g_n \\
+    \\
+    g^{*} \circ f^{*} : A \rightarrow T C \\
+    g^{*} \circ f^{*} = (g_0 \circ f_0) \times (g_1 \circ f_1) \times \dots \times (g_n \circ f_n)
+\end{eqnarray*}
 
 
 
-\section{Definition of Delta Monad}
-\section{An example of program includes modification}
-\section{DeltaM combinator with other Monads}
-\section{An example of program includes modification with traces}
-\section{Conclusion and future works}
-
 \appendix
 \section{Appendix Title}