Mercurial > hg > Papers > 2015 > atton-thesis

annotate english_presentation/slide.md @ 88:8d1325911030

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mini fixes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 19 Feb 2015 22:22:28 +0900
parents 65fdfe9c3997
children b29ab7ecf509
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 title: Categorical Formalization of Program Modification
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 author: Yasutaka Higa
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 profile : Concurrency Reliance Laboratory (Kono lab) <br> Department of Information Engineering <br> University of the Ryukyus
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 lang: English
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 # Formalization of Program Modification
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 * To improve the reliability of a program
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 * Development process has to be formalized
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 * Especially program modifications are important
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 * Let's formalize modification using Monad
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 # Formalization using Monad
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 * Monad is a notion of Category theory
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 * Monad represents meta computations in functional programming languages
88
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
15 * We proposed Delta Monad representation of program modifications
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 * We give definitions and the proof
88
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
17 * Delta Monad can be used with other monads
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 # Merits of formalizing program modifications
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 * Formal methods give verification of program based on mathematics and logics
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 * Such as lambda calculus and corresponding proofs
88
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
22 * Moggi[1989] , introduce Monad as notion of meta computation in program
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 * A meta computation represented as a Monad has one to one mapping
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 * We define program modification as meta computation which includes all modifications
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 # Definitions of Program
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 * A program is a typed lambda calculus
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 * lambda term
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 * variables : x,y
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 * function applications : f x
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 * lambda : \x -> f x
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 * type
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 * type variable : A, B
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 * functional type : A -> B
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 # Every lambda term has a type
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 y :: B
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 f :: A -> B
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 f x = y
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 * ``=`` is a function definition
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 * `` f x `` is a application function ``f``
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 * `` f x `` has type B
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 # Definition of Delta in Haskell
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 data Delta a = Mono a | Delta a (Delta a)
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 * ``data`` is a data type definition in Haskell
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 * `` a `` is a type variable
88
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
53 * `` Mono a`` and `` Delta a (Delta a) `` has a type `` Delta a``
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
54 * Delta can be stores all modification like list structure
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 # How to define meta computation in Haskell
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 * original function : f :: a -> b
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 * meta function : f' :: a -> Monad b
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 * Original function combination : f ( g ( x ))
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 * Meta function combination : (x >>= f') >>= g'
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 * f' returns various value which type is Monad
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 * Meta computation defined by f' and ``>>=``
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 * cf. ``>>=`` is an infix function
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 # Definition of Delta meta computation
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 >>= :: (Delta a) -> (a -> Delta b) -> (Delta b)
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 (Mono x) >>= f = f x
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 (Delta x d) >>= f = Delta (headDelta (f x))
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 (d >>= (tailDelta . f))
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 * Meta function f is applied to all the versions in a Delta Monad
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 * Delta data types is accessed by a pattern match
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 * ``headDelta`` takes first version of Delta
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 * ``tailDelta`` takes the rest versions
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 # An example of Program using Delta Monad
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 * Two versions of a simple program are shown
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 * Gives Delta Monad representation of the versions
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 * Various computation can be possible in the Delta
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
88
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
83 # An Example Program: numberCount (Version 1)
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 generator x = [1..x]
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 numberFilter xs = filter isPrime xs
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 count xs = length xs
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 numberCount x = count (numberFilter (generator x))
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92
88
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
93 # An Example Program: numberCount (Version 2)
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 generator x = [1..x]
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 numberFilter xs = filter even xs
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 count xs = length xs
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 numberCount x = count (numberFilter (generator x))
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 # An Example of Program includes two versions
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 generator x = Mono [1..x]
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 numberFilter xs = Delta (filter even xs)
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 (Mono (filter isPrime xs))
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 count x = Mono (length x)
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 numberCount x = count =<< numberFilter =<< generator x
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112
88
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
113 # Execution Program includes two version
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
114 * result
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
115 * Version 1 : 168
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
116 * Version 2 : 500
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117
88
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
118 ```
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
119 *Main> numberCount 1000
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
120 Delta 500 (Mono 168)
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
121 ```
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
122
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
123 # Combine Delta Monad with other Monads
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
124 * Delta Monad can be used with other monads
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
125 * Meta computations can be added function to Delta
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
126 * Exception, Logging , I/O
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
127
8d1325911030 Mini fixes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
128 # An Example Delta Monad with Traces
87
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 *Main> numberCountM 10
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]",
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 "[2,3,5,7]",
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 "4"]))
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 (Mono (Writer (5, ["[1,2,3,4,5,6,7,8,9,10]",
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 "[2,4,6,8,10]",
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136 "5"]))))
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 ```
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 # How to use Delta Monad in program development
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 * Executing selected versions
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 * Comparing traces of versions
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 * Version Control Systems are formalized by Delta Monad
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 * Combination of other Monads make development more reliable
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 # Conclusion
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 * Program Modifications are formal defined
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 * Program Modifications are meta computation
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 * Program Modifications are Delta Monad
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 * Monad-laws are proved in Agda
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 * Delta Monad include all necessary aspects of modifications?
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 * What is products/colimits over program versions?
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152
65fdfe9c3997 Add slide in English
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 <!-- vim: set filetype=markdown.slide: -->