--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/english_presentation/slide.md	Thu Feb 19 20:24:16 2015 +0900
@@ -0,0 +1,141 @@
+title: Categorical Formalization of Program Modification
+author: Yasutaka Higa
+profile : Concurrency Reliance Laboratory (Kono lab) <br> Department of Information Engineering <br> University of the Ryukyus
+lang: English
+
+# Formalization of Program Modification
+* To improve the reliability of a program
+* Development process has to be formalized
+* Especially program modifications are important
+* Let's formalize modification using Monad
+
+# Formalization using Monad
+* Monad is a notion of Category theory
+* Monad represents meta computations in functional programming languages
+* We proposed delta monad representation of program modifications
+* We give definitions and the proof
+* Delta monad can be used with other monads
+
+# Merits of formalizing program modifications
+* Formal methods give verification of program based on mathematics and logics
+* Such as lambda calculus and corresponding proofs
+* Moggi[1990] , introduce Monad as notion of meta computation in program
+* A meta computation represented as a Monad has one to one mapping
+* We define program modification as meta computation which includes all modifications
+
+# Definitions of Program
+* A program is a typed lambda calculus
+* lambda term
+    * variables : x,y
+    * function applications : f x
+    * lambda : \x -> f x
+* type
+    * type variable   : A, B
+    * functional type : A -> B
+
+# Every lambda term has a type
+```
+    y   :: B
+    f   :: A -> B
+    f x = y
+```
+* ``=`` is a function definition
+* `` f x `` is a application function ``f``
+* `` f x `` has type B
+
+# Definition of Delta in Haskell
+```
+data Delta a = Mono a | Delta a (Delta a)
+```
+
+* ``data`` is a data type definition in Haskell
+* `` a `` is a type variable
+* `` Mono a`` has a type `` Delta a``
+* `` Delta a (Delta a) `` has a type ``Delta a``
+
+# How to define meta computation in Haskell
+* original function : f  :: a -> b
+* meta function     : f' :: a -> Monad b
+* Original function combination : f ( g ( x ))
+* Meta function combination : (x >>= f') >>= g'
+* f' returns various value which type is Monad
+* Meta computation defined by f' and ``>>=``
+* cf. ``>>=`` is an infix function
+
+# Definition of Delta meta computation
+```
+ >>= :: (Delta a) -> (a -> Delta b) -> (Delta b)
+ (Mono x)    >>= f = f x
+ (Delta x d) >>= f = Delta (headDelta (f x))
+                           (d >>= (tailDelta . f))
+```
+
+* Meta function f is applied to all the versions in a Delta Monad
+* Delta data types is accessed by a pattern match
+* ``headDelta`` takes first version of Delta
+* ``tailDelta`` takes the rest versions
+
+# An example of Program using Delta Monad
+* Two versions of a simple program are shown
+* Gives Delta Monad representation of the versions
+* Various computation can be possible in the Delta
+
+# numberCount (Version 1)
+
+```
+generator x     = [1..x]
+numberFilter xs = filter isPrime xs
+count xs        = length xs
+
+numberCount x = count (numberFilter (generator x))
+```
+
+# numberCount (Version 2)
+
+```
+generator x     = [1..x]
+numberFilter xs = filter even xs
+count xs        = length xs
+
+numberCount x = count (numberFilter (generator x))
+```
+
+# An Example of Program includes two versions
+```
+generator x     = Mono [1..x]
+numberFilter xs = Delta (filter even xs)
+                        (Mono (filter isPrime xs))
+count x         = Mono (length x)
+
+numberCount x = count =<< numberFilter =<< generator x
+```
+
+# Combine Delta Monad and other Monads
+* TODO
+
+# Example
+```
+*Main> numberCountM 10
+DeltaM (Delta (Writer (4, ["[1,2,3,4,5,6,7,8,9,10]",
+                           "[2,3,5,7]",
+                           "4"]))
+       (Mono  (Writer (5, ["[1,2,3,4,5,6,7,8,9,10]",
+                           "[2,4,6,8,10]",
+                           "5"]))))
+```
+
+# How to use Delta Monad in program development
+* Executing selected versions
+* Comparing traces of versions
+* Version Control Systems are formalized by Delta Monad
+* Combination of other Monads make development more reliable
+
+# Conclusion
+* Program Modifications are formal defined
+* Program Modifications are meta computation
+* Program Modifications are Delta Monad
+* Monad-laws are proved in Agda
+* Delta Monad include all necessary aspects of modifications?
+* What is products/colimits over program versions?
+
+<!-- vim: set filetype=markdown.slide: -->