Mercurial > hg > Papers > 2015 > atton-icfp

comparison delta.tex @ 5:87bb6169c80d default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing ...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Fri, 27 Feb 2015 17:07:58 +0900
parents ecebdd7bfa48
children
comparison
equal deleted inserted replaced
4:ecebdd7bfa48 5:87bb6169c80d
70 We define meta computation notated modifications list like structure named Delta Monad. 70 We define meta computation notated modifications list like structure named Delta Monad.
71 71
72 Delta Monad represents modifications by accumulates all versions of a program. 72 Delta Monad represents modifications by accumulates all versions of a program.
73 Accumulated modifications can computes by meta computation. 73 Accumulated modifications can computes by meta computation.
74 In this paper, We propose meta computation execute a program includes modifications simultaneously on Delta. 74 In this paper, We propose meta computation execute a program includes modifications simultaneously on Delta.
75 Additionally, Delta Monad can be used with other Monads for more computations of modifications.
76 75
77 \section{Programs and Monads} 76 \section{Programs and Monads}
78 Programs notated typed lambda calculus constructed values and abstractions. 77 Programs notated typed lambda calculus constructed values and abstractions.
79 Abstractions maps value to value. 78 Abstractions maps value to value.
79 Abstraction f applies to x notated $ f x $.
80 Every lambda term has a type. 80 Every lambda term has a type.
81 Value x has type A notated $ x : A $. 81 Value x has type A notated $ x : A $.
82 Abstraction f has a argument of type A and return value of type B notated $ f : A \rightarrow B $. 82 Abstraction f has a argument of type A and return value of type B notated $ f : A \rightarrow B $.
83 83
84 \begin{eqnarray} 84 \begin{eqnarray*}
85 x : A \\ 85 x : A \\
86 f : A \rightarrow B \\ 86 f : A \rightarrow B \\
87 f x : B 87 f x : B \\
88 \end{eqnarray} 88 \end{eqnarray*}
89 89
90 Execution of a program is application of abstraction. 90 Type matched abstractions can be composed by operator ';'.
91 Some computations can not be notated abstraction like Input/Output are meta computation. 91 Order of composition are commutative.
92 Meta computations are computations for implements computations. 92
93 \begin{eqnarray*}
94 f : A \rightarrow B \\
95 g : B \rightarrow C \\
96 f;g : A \rightarrow C \\
97 \\
98 h : C \rightarrow D \\
99 (f;g);h = f;(g;h)
100 \end{eqnarray*}
101
102 Abstractions can be extended using Monad.
103
104 Monad is $ triple (T, \eta, \mu) $ satisfies laws(Figure) % TODO :commutative diagram
105 Various meta computations represents by definition of triple.
106 Monad has another description Kleisli Triple $ (T, \eta, \_^{*}) $.
107 Kleisli triple are following equations hold:
108
109 \begin{itemize}
110 \item $ \eta^{*}_A = id_{T A} $
111 \item $ \eta;f^{*} = f \mbox{ for } f : A \rightarrow T B $
112 \item $ f^{*} ; g^{*} = (f; g^{*})^{*} \mbox{ for } f : A \rightarrow T B \mbox{ and } g : B \rightarrow T C $
113 \end{itemize}
114
115 Kleisli Triple can build from Monad ($ (T, \eta, \mu) $).
116
117 For Example, definition of diverging computation using Monad are shown.
118
119 \begin{itemize}
120 \item $ T A = A_{\bot} (= A + \{\bot\}) $
121 \item $ \eta_A $ is the inclusion of A into $ A_{\bot} $
122 \item if $ f : A \rightarrow T B $, then $ f^{*} (\bot) = \bot $ and $ f^{*}(a) = f (a) $ when $ a $ has type A.
123 \end{itemize}
124
125 \section{Modification using Monad}
126
127 \begin{equation*}
128 T A = A_0 \times A_1 \times \dots \times A_n
129 \end{equation*}
130
131 \begin{eqnarray*}
132 x : A \\
133 x^{*} : T A \\
134 x^{*} : A_0 \times A_1 \times \dots \times A_n \\
135 \\
136 f : A \rightarrow B \\
137 f^{*} : A \rightarrow T B \\
138 f^{*} : (A_0 \rightarrow B_0) \times (A_1 \rightarrow B_1) \times \dots \times (A_n \rightarrow B_n)
139 \end{eqnarray*}
140
141 \begin{eqnarray*}
142 f^{*} : A \rightarrow T B \\
143 f^{*} = f_0 \times f_1 \times \dots f_n \\
144 \\
145 g^{*} : B \rightarrow T C \\
146 g^{*} = g_0 \times g_1 \times \dots g_n \\
147 \\
148 g^{*} \circ f^{*} : A \rightarrow T C \\
149 g^{*} \circ f^{*} = (g_0 \circ f_0) \times (g_1 \circ f_1) \times \dots \times (g_n \circ f_n)
150 \end{eqnarray*}
93 151
94 152
95
96 \section{Definition of Delta Monad}
97 \section{An example of program includes modification}
98 \section{DeltaM combinator with other Monads}
99 \section{An example of program includes modification with traces}
100 \section{Conclusion and future works}
101 153
102 \appendix 154 \appendix
103 \section{Appendix Title} 155 \section{Appendix Title}
104 156
105 This is the text of the appendix, if you need one. 157 This is the text of the appendix, if you need one.