--- a/cfopm.tex	Fri Apr 17 15:23:34 2015 +0900
+++ b/cfopm.tex	Fri Apr 17 17:02:20 2015 +0900
@@ -92,9 +92,76 @@
 Meta computations contains various computations including partiality, nondeterminism, side-effects, exceptions and continuations.
 
 \section{Meta computation and Monads}
-Meta computations in CbC formalized by Monads so prevent chaos by unlimited computations.
+Meta computations in CbC formalized by Monads to prevent chaos by unlimited computations.
 Monads are a notion of Category Theory, in programs Monad correspondence of normal/meta computations.
-For example, function can fail is represented direct sum of values and bottom.
+For example, diverging computation as extended normal computations is represented direct sum of normal values and bottom.
+
+We show formalization of programs for using Monads.
+Programs notated typed lambda calculus constructed values and abstractions.
+Abstraction f maps value to value, and applies to value 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*}
+    x : A \\
+    f : A \rightarrow B \\
+    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 has many arguments notated by abstraction took a argument, and returns a abstraction that argument numbers has decreased(Currying).
+
+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}
+
+$ id $ is abstraction that identity mapping for any typed values ($ id x = x $).
+$ id $ was exists any typed values.
+notation $ id_{X} x $ is application $ id $ to a value x typed X.
+Then, $ T $ is functor that pair of structure and a map that abstraction for non-structured values to abstraction for structured values.
+if applied functor T to type A notated $ T A $.
+For example, list of any types is functor.
+List can be constructed to any typed values (list of characters, list of integers ...) and can be apply abstraction for contains elements.
+
+\begin{eqnarray*}
+    xs = \verb/[10 , 20 , 30]/ \\
+    xs : \verb/List Int/ \\
+    f  : \verb/Int/ \rightarrow \verb/String/ \\
+    \verb/[f 10 , f 20 , f 30]/ : \verb/List String/
+\end{eqnarray*}
+
+It's summarized informal definition of functor for explain Monad.
+Values extended using property of functor T extend abstraction to normal values to structured values.
+
+Abstraction extended by $ \_^{*} $ on Kleisli Triple build from Monad $ (T, \eta, \mu) $.
+For Example, definition of diverging computation using Monad are shown.
+
+\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 of Programs using a Monad}