Binary file cfopm.pdf has changed

--- a/cfopm.tex	Sun Apr 19 20:32:27 2015 +0900
+++ b/cfopm.tex	Mon Apr 20 10:31:10 2015 +0900
@@ -104,8 +104,8 @@
 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. 
+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.
@@ -119,9 +119,9 @@
 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.
+Program modifications are defined as Monad which contains previous versions of the functions.
 In this way, program modifications are represented as a meta computation.
-For example, We an execute multi versions simultaneously using this Monad.
+For example, We can execute multi versions simultaneously using this Monad.
 
 \section{Meta computation and a Monad}
 Meta computations in CbC are formalized by Monad.
@@ -137,13 +137,9 @@
 Composition of arrows and its association laws are provided.
 
 
-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.
-
-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.
+If you have a function f which domain is A and codomain is B,
+    $ f :: A \rightarrow 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.
 
@@ -152,43 +148,62 @@
 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*}
+\begin{align*}
     x :: A \\
     f :: A \rightarrow B \\
     f x :: B \\
-\end{eqnarray*}
+\end{align*}
 
-Function composition operator is '.'.
+
+Function composition operator is ``.`` .
 As usual order of composition are associative.
 
-\begin{eqnarray*}
-    f : A \rightarrow B \\
-    g : B \rightarrow C \\
-    g \circ f : A \rightarrow C \\
+\begin{align*}
+    f :: A \rightarrow B \\
+    g :: B \rightarrow C \\
+    g \circ f :: A \rightarrow C \\
     \\
-    h : C \rightarrow D \\
-    (h \circ g) \circ f = h \circ (g \circ f) : A \rightarrow D
-\end{eqnarray*}
+    h :: C \rightarrow D \\
+    (h . g) . f = h . (g . f) :: A \rightarrow D
+\end{align*}
+
+Sum type is introduced using Haskel syntax(Table\ref{src:delta_data_definition}).
 
-Sum type is introduced using Haskel syntax.
-
-    data Delta a = Mono a
-                 | Delta a (Delta a)
+\begin{table}[html]
+\begin{lstlisting}
+data Delta a = Mono a
+             | Delta a (Delta a)
+\end{lstlisting}
+\label{src:delta_data_definition}
+\caption{Definition of data type ``Delta`` in Haskell}
+\end{table}
 
 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.
+{\tt Mono a} and {\tt Delta a} is a constructor of data type {\tt Delta}, which maps object a in a category to object {\tt 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(Table \ref{src:delta_fmap}).
 
-    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)
+\begin{table}[html]
+\begin{lstlisting}
+deltaFmap :: (a -> b) -> Delta a -> Delta b
+deltaFmap f (Mono x)    = Mono (f x)
+deltaFmap f (Delta x d) = Delta (f x) (deltaFmap f d)
+\end{lstlisting}
+\label{src:delta_fmap}
+\caption{Arrow mapping for data type ``Delta``}
+\end{table}
 
 Arrow mapping in a functor satisfies identity law and distribution law.
-Data type can be accessed by pattern matching.
+Data type can be accessed by pattern matching(Table\ref{src:head_delta}).
 
-    headDelta :: Delta a -> a
-    headDelta (Mono  x)   = x
-    headDelta (Delta x d) = x
+\begin{table}[html]
+\begin{lstlisting}
+headDelta :: Delta a -> a
+headDelta (Mono  x)   = x
+headDelta (Delta x d) = x
+\end{lstlisting}
+\label{src:head_delta}
+\caption{Define function to Delta using pattern matching}
+\end{table}
 
 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.
@@ -203,33 +218,35 @@
 Monad also satisfies to laws below:
 
 \begin{itemize}
-    \item association law : $ {\mu}_{A}  \circ {\mu}_{T A} = {\mu}_{A} \circ T {\mu}_{A} $
-    \item unity law : $ {\mu}_{A} \circ \eta_{T A} = \mu_{A} \circ T \eta_{A} = id_{T A} $
+    \item association law : $ {\mu}_{A}  . {\mu}_{T A} = {\mu}_{A} . T {\mu}_{A} $
+    \item unity law : $ {\mu}_{A} . \eta_{T A} = \mu_{A} . T \eta_{A} = id_{T A} $
 \end{itemize}
 
 Various meta computations represents by definition of triple.
-For each function f :: A -> B, there is a meta computation f* :: A -> T B.
-Combination of f* g* is defined as follows:
+For each function $ f :: A \rightarrow B $ , there is a meta computation $ f^* :: A \rightarrow T B $.
+Combination of $ f^* $ $ g^*$ is defined as follows:
+
+\begin{align*}
+    f^* . g^* = \mu (deltaFmap f^* (\mu (deltaFmap g^*)))
+\end{align*}
 
-    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.
+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.
 
-Normal function f has a meta function f* which returns Monad T.
+Normal function f has a meta function $ f^* $ which returns Monad T.
 
-% Remove description Kleisli category 
+% Remove description Kleisli category
 
 % 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.
@@ -237,21 +254,21 @@
 % 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} $
@@ -277,15 +294,17 @@
 
 \begin{table}[html]
 \begin{lstlisting}
-data Delta a = Mono a | Delta a (Delta a)
+data Delta a = Mono a
+             | Delta a (Delta a)
+             deriving Show
 
 headDelta :: Delta a -> a
 headDelta (Mono  x)   = x
-headDelta (Delta x _) = x
+headDelta (Delta x d) = x
 
 tailDelta :: Delta a -> Delta a
 tailDelta (Mono x)     =  Mono x
-tailDelta (Delta _ ds) = ds
+tailDelta (Delta d ds) = ds
 
 instance Monad Delta where
   return x           = Mono x
@@ -298,16 +317,36 @@
 \end{table}
 
 Modifications of values are stored as a list like structure.
-Delta contains two constructor Mono and Delta, Mono represents first version, Delta represents modification.
-% FIXME
-Infix operator \verb/>>=/ handles extended functions has typed $ \verb/A/ \rightarrow \verb/Delta B/ $ recursive applies to each original versions.
+Delta contains two constructor {\tt Mono} and {\tt Delta}, {\tt Mono} represents first version, {\tt Delta} represents modification.
+Infix operator \verb/>>=/ handles meta functions has typed $ A \rightarrow 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 proved satisfying Monad laws by proof assistant language Agda\cite{agda}.
 This monad can be combined with other Monad such as Writer.
 
+% FIXME: please check added an example
 \section{Example}
 
-% +2, *2
+\begin{table}[html]
+\begin{lstlisting}
+-- functiion version one. add 2 to integer.
+f :: Int -> Int
+f x = x + 2
+
+-- function version two. multiply 3 to integer.
+f2 :: Int -> Int
+f2 x = x * 3
+
+-- meta function contains two version.
+f' :: Int -> Delta Int
+f' x = Delta (x + 2) (Mono (x * 3))
+
+-- We can execute multi versions simultaneously.
+-- *Main> Mono 100 >>= f'
+-- Delta 102 (Mono 300)
+\end{lstlisting}
+\label{src:example_delta}
+\caption{An Example using Delta}
+\end{table}
 
 \section{Conclusion and Future Works}
 Program modification is defined as a Monad.