changeset 7:5ecae062b32b

Writing third chapter ...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 17 Apr 2015 19:06:36 +0900
parents 1e3b7eb09712
children b172215a69d5
files cfopm.tex
diffstat 1 files changed, 78 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/cfopm.tex	Fri Apr 17 17:02:20 2015 +0900
+++ b/cfopm.tex	Fri Apr 17 19:06:36 2015 +0900
@@ -2,7 +2,30 @@
 
 \usepackage[cmex10]{amsmath}
 \usepackage{url}
+\usepackage{listings}
 
+\lstset{
+  frame=single,
+  keepspaces=true,
+  stringstyle={\ttfamily},
+  commentstyle={\ttfamily},
+  identifierstyle={\ttfamily},
+  keywordstyle={\ttfamily},
+  basicstyle={\ttfamily},
+  breaklines=true,
+  xleftmargin=0zw,
+  xrightmargin=0zw,
+  framerule=.2pt,
+  columns=[l]{fullflexible},
+  numbers=left,
+  stepnumber=1,
+  numberstyle={\scriptsize},
+  numbersep=1em,
+  language={},
+  tabsize=4,
+  lineskip=-0.5zw,
+  escapechar={@},
+}
 
 \ifCLASSINFOpdf
   % \usepackage[pdftex]{graphicx}
@@ -42,15 +65,12 @@
 % author names and affiliations
 % use a multiple column layout for up to three different
 % affiliations
-\author{\IEEEauthorblockN{Yasutaka HIGA}
-\IEEEauthorblockA{
-University of the Ryukyus \\
-Email: atton@cr.ie.u-ryukyu.ac.jp}
+\author{
+\IEEEauthorblockN{Yasutaka HIGA}
+\IEEEauthorblockA{University of the Ryukyus \\ Email: atton@cr.ie.u-ryukyu.ac.jp}
 \and
 \IEEEauthorblockN{Shinji KONO}
-\IEEEauthorblockA{
-University of the Ryukyus \\
-Email: kono@ie.u-ryukyu.ac.jp}
+\IEEEauthorblockA{University of the Ryukyus \\ Email: kono@ie.u-ryukyu.ac.jp}
 }
 
 % make the title area
@@ -79,7 +99,7 @@
 
 \section{Continuation based C}  % enough only describe code/data segment?
 We proposed programming style using unit of program named code segment and data segment. % TODO: ref
-Code segment is a unit of calculation is not dependents state.
+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.
@@ -138,11 +158,11 @@
 
 $ 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.
+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 $.
+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.
+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]/ \\
@@ -153,9 +173,10 @@
 
 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) $
 
-Abstraction extended by $ \_^{*} $ on Kleisli Triple build from Monad $ (T, \eta, \mu) $.
-For Example, definition of diverging computation using Monad are shown.
+Definition of diverging computation as extend normal computations using Monad are shown.
 
 \begin{itemize}
     \item $ T A = A_{\bot} (= A + \{\bot\}) $
@@ -163,8 +184,51 @@
     \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}
+\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:
+
+\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}).
+
+\begin{table}[html]
+\begin{lstlisting}
+data Delta a = Mono a | Delta a (Delta a)
 
+headDelta :: Delta a -> a
+headDelta (Mono  x)   = x
+headDelta (Delta x _) = x
+
+tailDelta :: Delta a -> Delta a
+tailDelta (Mono x)     =  Mono x
+tailDelta (Delta _ ds) = ds
+
+instance Monad Delta where
+  return x           = Mono x
+  (Mono x) >>= f     = f x
+  (Delta x d) >>= f  = Delta (headDelta (f x))
+                             (d >>= (tailDelta . f))
+\end{lstlisting}
+    \label{src:delta_monad}
+    \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.
+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.
 
 % An example of a floating figure using the graphicx package.
 % Note that \label must occur AFTER (or within) \caption.