--- a/cfopm.tex	Sun Apr 19 17:17:16 2015 +0900
+++ b/cfopm.tex	Sun Apr 19 20:32:27 2015 +0900
@@ -97,40 +97,69 @@
 % creates the second title. It will be ignored for other modes.
 \IEEEpeerreviewmaketitle
 
-\section{Continuation based C}  % enough only describe code/data segment?
-We proposed programming style using unit of program named code segment and data segment.
-Code segment is a unit of calculation not dependents state.
-Data segment contains values of calculation and calculation context called meta data segment.
-Execution of program is represented by moves interconnected code segments.
-Code/Data segment style programming was suitable to state based concurrent program.
+\section{Continuation based C}
+We proposed units of program named code segment and data segment.
+Code segment is a unit of calculation which has no state.
+Data segment is a set of typed data.
+Code segments are connected to data segments with a context, which is a meta data segment.
+After an execution of a code segment and its context, next code segments (Continuation) is executed.
+
+We had developed a programming language 'Continuation based C' \cite{DBLP:journals/corr/abs-1109-4048},
+hear after we call it CbC, which supports code segments. 
+CbC is compatible with C language and it has continuation as a goto statement.
+Actually, goto statements are tail call of another a code segment and a code segment is a C function.
+Tail call elimination is forced by our LLVM based compiler.
+We are currently designing data segments part on CbC.
+
+Code segments and data segments are low level enough to represent computation details,
+and it is architecture independent.
+It can be used as an architecture independent assembler.
+
+In this paper, meta computation of CbC is discussed.
+We introduce meta computation as a Monad.
+As an example, versioning of functions are represented as a Monad.
+Reliability of a program strongly depends on a method of modification.
+Program modifications are defined as Monad which contains previous versions of the function.
+In this way, program modifications are represented as a meta computation.
+For example, We an execute multi versions simultaneously using this Monad.
 
-Programming language 'Continuation based C' (CbC\cite{DBLP:journals/corr/abs-1109-4048}) supported code/data segment style programming.
-CbC is lower language of C removed function call and loop-statements(for, while) and added continuation by goto and code segment.
-Code segment of CbC is function without return values in C.
-Interconnections of code segment represents goto with environment.
-CbC can define meta calculation as calculation of calculation named meta code segment.
-Meta computations contains various computations including partiality, nondeterminism, side-effects, exceptions and continuations.
+\section{Meta computation and a Monad}
+Meta computations in CbC are formalized by Monad.
+At first, we review meta computation and Monad.
+
+Monad is a notion of Category Theory.
+
+A category contains arrows and objects.
+Arrow in a category is function.
+Objects in a category is types.
+A function has its input type and its output type,
+so an arrow in a category has domain object and codomain object.
+Composition of arrows and its association laws are provided.
+
 
-\section{Meta computation and Monads}
-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\cite{Moggi:1991:NCM:116981.116984}.
-For example, diverging computation is represented direct sum of normal values and bottom.
+Functor is a data type which has a type variable.
+Monad is a functor which satisfies Monad laws.
+Monad laws contains natural transformations, eta and mu.
 
-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 $.
+If you have a function f which domain is A and codomain is B, 
+    f :: A -> B
+Then, there are meta function f* which codomain is T B.
+In this way, normal computation and meta computation as one to one correspondence\cite{Moggi:1991:NCM:116981.116984}.
+Various computations such as partiality, nondeterminism, side-effects, exceptions and continuations are represented as Monads.
+
+We use typed lambda calculus as a representation of function and Haskell syntax is used.
+Programs notated typed lambda calculus constructed values and functions.
+Value x has a type A is notated as $ x :: A $.
+An application of a function f to value x is notated as $ f x $.
 
 \begin{eqnarray*}
-    x : A \\
-    f : A \rightarrow B \\
-    f x : B \\
+    x :: A \\
+    f :: A \rightarrow B \\
+    f x :: B \\
 \end{eqnarray*}
 
-Type matched abstractions can be composed by operator '$\circ$'.
-Order of composition are commutative.
+Function composition operator is '.'.
+As usual order of composition are associative.
 
 \begin{eqnarray*}
     f : A \rightarrow B \\
@@ -141,10 +170,37 @@
     (h \circ g) \circ f = h \circ (g \circ f) : A \rightarrow D
 \end{eqnarray*}
 
-Abstractions has many arguments notated by abstraction took a argument, and returns a abstraction that argument numbers has decreased(Currying).
+Sum type is introduced using Haskel syntax.
+
+    data Delta a = Mono a
+                 | Delta a (Delta a)
+
+This is data type definition of sum type delta which has type variable {\tt a}.
+Mono a and Delta a is a constructor of data type Delta, which maps object a in a category to object Delta a in the same category.
+Functor is a mapping from category A to B, which has two mappings, one for object mapping and one for arrow mapping.
+
+    fmap-delta :: (a -> b) -> Delta a -> Delta b
+    fmap-delta f (Mono x)    = Mono (f x)
+    fmap-delta f (Delta x d) = Delta (f x) (fmap-delta f d)
+
+Arrow mapping in a functor satisfies identity law and distribution law.
+Data type can be accessed by pattern matching.
 
-Abstractions can be extended using Monad.
-Monad is $ triple (T, \eta, \mu) $ satisfies laws.
+    headDelta :: Delta a -> a
+    headDelta (Mono  x)   = x
+    headDelta (Delta x d) = x
+
+This is a natural transformation from functor Delta to identity functor.
+Natural transformation is a set of arrow between two functors, which satisfies commutative law.
+%   f (headDelta x) = headDelta (delta-fmap f x)
+
+Monad in category A is $ triple (T, \eta, \mu) $.
+T is a functor from A to A.
+eta is a natural transformation from identity functor to T.
+mu is a natural transformation from TT to T.
+TT is a nested data structure of T.
+
+Monad also satisfies to laws below:
 
 \begin{itemize}
     \item association law : $ {\mu}_{A}  \circ {\mu}_{T A} = {\mu}_{A} \circ T {\mu}_{A} $
@@ -152,62 +208,72 @@
 \end{itemize}
 
 Various meta computations represents by definition of triple.
-Monad has another description Kleisli Triple $ (T, \eta, \_^{*}) $.
-
-Kleisli triple are following equations hold:
+For each function f :: A -> B, there is a meta computation f* :: A -> T B.
+Combination of f* g* is defined as follows:
 
-\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}
+    f* . g* = mu (delta-fmap f* (mu (delta-fmap g*)))
+    
+Association law of f* is derived from Monad laws.
+In this way, for each Monad there is a new category of f* which is a well known Kleisli Category.
 
-$ 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, etc) and can be apply abstraction for stored elements.
+Normal function f has a meta function f* which returns Monad T.
+
+% Remove description Kleisli category 
 
-\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.
-Kleisli triple $ (T, \eta, \_^{*}) $ are a triple of functor T and $ \eta $ extension of normal values to meta one and $ \_^{*} $ extension of abstraction.
-Kleisli triple are derivable from Monad $ (T, \eta, \mu) $
-
-Definition of diverging computation as extend normal computations 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}
+% 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, etc) and can be apply abstraction for stored 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.
+% Kleisli triple $ (T, \eta, \_^{*}) $ are a triple of functor T and $ \eta $ extension of normal values to meta one and $ \_^{*} $ extension of abstraction.
+% Kleisli triple are derivable from Monad $ (T, \eta, \mu) $
+% 
+% Definition of diverging computation as extend normal computations 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 Program using Monad}
-Reliability of a program dynamically changed in software development.
-We propose handle modifications of a program as meta computations for improve reliability.
-Modifications represents a set of program versions including values and abstraction with type consistency.
-Execution of program including modification like concurrent execution of all versions.
-
-Definition of modifications named 'Delta Monad' are shown:
+A program is set of function.
+Modifications of a program are set of mapping from old version of functions to new functions.
+These versions may have different types or same types and each version have correct type matchings.
 
-\begin{itemize}
-    \item $ T A = A_0 \times A_1 \times \dots \times A_n $
-    \item $ \eta_A $ is map to values accumulated modification.
-    \item if $ f : A \rightarrow T B $ and $ x : T A  $ then \\
-        $ f^{*}(x) = \langle f_0(x_0) , f_1(x_1), \dots, f_n(x_n) \rangle$
-\end{itemize}
+% Definition of modifications named 'Delta Monad' are shown:
+% \begin{itemize}
+%     \item $ T A = A_0 \times A_1 \times \dots \times A_n $
+%     \item $ \eta_A $ is map to values accumulated modification.
+%     \item if $ f : A \rightarrow T B $ and $ x : T A  $ then \\
+%         $ f^{*}(x) = \langle f_0(x_0) , f_1(x_1), \dots, f_n(x_n) \rangle$
+% \end{itemize}
 
-Versions of a program without branching represents finite direct product.
+
 
-We simulated Delta Monad in Haskell (Table\ref{src:delta_monad}).
+In case of modification with no type changes, Delta Monad is defined as a program modification as follows:
 
 \begin{table}[html]
 \begin{lstlisting}
@@ -231,18 +297,28 @@
     \caption{Definition of Delta Monad in Haskell}
 \end{table}
 
-We aim to prove Delta Monads satisfies Monad laws using Haskell has built-in Monad definition.
-Modifications of values stored list like structure named Delta.
+Modifications of values are stored as a list like structure.
 Delta contains two constructor Mono and Delta, Mono represents first version, Delta represents modification.
-Infix operator \verb/>>=/ handles extended abstraction has typed $ \verb/A/ \rightarrow \verb/Delta B/ $ recursive applies to each original versions.
+% FIXME
+Infix operator \verb/>>=/ handles extended functions has typed $ \verb/A/ \rightarrow \verb/Delta B/ $ recursive applies to each original versions.
 This definition represents simple modification only monotonic increase versioning (exclude branching and merging) and program has consistent type in all versions.
-We executed different versions in same time and proved satisfying Monad laws by proof assistant language Agda\cite{agda}.
+We proved satisfying Monad laws by proof assistant language Agda\cite{agda}.
+This monad can be combined with other Monad such as Writer.
+
+\section{Example}
+
+% +2, *2
 
 \section{Conclusion and Future Works}
-Handleable modification by meta computations is proposed.
-Using this Delta Monad, we can make reliable program development possible.
-Especially, Automatically property comparison in development cycle is made possible by CbC also plans incorporate model checker as meta computations.
-We aim to extend Delta Monad represents all possible modifications (branching, merging, and more) with proof and implement to CbC.
+Program modification is defined as a Monad.
+Modifications as meta computations makes various checking methods possible.
+These checking methods are also some kind of Monads.
+In this way, we can provide program development tool based on categorical formulation.
+We are implementing various methods in CbC.
+In this paper, we only handles modification on the same types.
+Formulation of Modifications on the different types will be proposed in future.
+Only linear version structure handled here.
+We hope that more complex structure such as branching or merging can be handle in the same way.
 
 
 % An example of a floating figure using the graphicx package.