Mercurial > hg > Papers > 2015 > atton-lola
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.