### changeset 5:87bb6169c80ddefaulttip

Writing ...
author Yasutaka Higa Fri, 27 Feb 2015 17:07:58 +0900 ecebdd7bfa48 delta.tex 1 files changed, 65 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/delta.tex	Thu Feb 26 17:57:31 2015 +0900
+++ b/delta.tex	Fri Feb 27 17:07:58 2015 +0900
@@ -72,33 +72,85 @@
Delta Monad represents modifications by accumulates all versions of a program.
Accumulated modifications can computes by meta computation.
In this paper, We propose meta computation execute a program includes modifications simultaneously on Delta.
-Additionally, Delta Monad can be used with other Monads for more computations of modifications.

\section{Programs and Monads}
Programs notated typed lambda calculus constructed values and abstractions.
Abstractions maps value to value.
+Abstraction f applies to 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}
+\begin{eqnarray*}
x : A \\
f : A \rightarrow B \\
-    f x : B
-\end{eqnarray}
+    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 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}
+
+Kleisli Triple can build from Monad ($(T, \eta, \mu)$).
+
+For Example, definition of diverging computation using Monad are shown.

-Execution of a program is application of abstraction.
-Some computations can not be notated abstraction like Input/Output are meta computation.
-Meta computations are computations for implements computations.
+\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 using Monad}
+
+\begin{equation*}
+    T A = A_0 \times A_1 \times \dots \times A_n
+\end{equation*}
+
+\begin{eqnarray*}
+    x : A \\
+    x^{*} : T A \\
+    x^{*} : A_0 \times A_1 \times \dots \times A_n \\
+    \\
+    f : A \rightarrow B \\
+    f^{*} : A \rightarrow T B \\
+    f^{*} : (A_0 \rightarrow B_0) \times (A_1 \rightarrow B_1) \times \dots \times (A_n \rightarrow B_n)
+\end{eqnarray*}
+
+\begin{eqnarray*}
+    f^{*} : A \rightarrow T B \\
+    f^{*} = f_0 \times f_1 \times \dots f_n \\
+    \\
+    g^{*} : B \rightarrow T C \\
+    g^{*} = g_0 \times g_1 \times \dots g_n \\
+    \\
+    g^{*} \circ f^{*} : A \rightarrow T C \\
+    g^{*} \circ f^{*} = (g_0 \circ f_0) \times (g_1 \circ f_1) \times \dots \times (g_n \circ f_n)
+\end{eqnarray*}

-\section{Definition of Delta Monad}
-\section{An example of program includes modification}
-\section{DeltaM combinator with other Monads}
-\section{An example of program includes modification with traces}
-\section{Conclusion and future works}
-
\appendix
\section{Appendix Title}