Mercurial > hg > Papers > 2015 > atton-thesis
view english_presentation/slide.md @ 87:65fdfe9c3997
Add slide in English
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 19 Feb 2015 20:24:16 +0900 |
parents | |
children | 8d1325911030 |
line wrap: on
line source
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: -->