Mercurial > hg > Papers > 2015 > atton-thesis

<!DOCTYPE HTML>

<html lang="English">
<head>
	<title>Categorical Formalization of Program Modification</title>
	<meta charset="UTF-8">
	<meta name="viewport" content="width=1274, user-scalable=no">
	<meta name="generator" content="Slide Show (S9)">
	<meta name="author" content="Yasutaka Higa">
	<link rel="stylesheet" href="themes/ribbon/styles/style.css">
	<link rel="stylesheet" href="slide.css">
</head>
<body class="list">
	<header class="caption">
		<h1>Categorical Formalization of Program Modification</h1>
		<p>Yasutaka Higa</p>
	</header>
	<div class="slide cover" id="Cover"><div>
		<section>
			<header>
				<h2>Categorical Formalization of Program Modification</h2>
				<h3 id="author">Yasutaka Higa</h3>
				<h3 id="profile">Concurrency Reliance Laboratory (Kono lab) <br> Department of Information Engineering <br> University of the Ryukyus</h3>
			</header>
		</section>
	</div></div>

<!-- todo: add slide.classes to div -->
<!-- todo: create slide id from header? like a slug in blogs? -->

<div class="slide" id="2"><div>
		<section>
			<header>
				<h1 id="formalization-of-program-modification">Formalization of Program Modification</h1>
			</header>
			<!-- === begin markdown block ===

      generated by markdown 1.1.1 on Ruby 2.2.0 (2014-12-25) [x86_64-darwin13]
                on 2015-02-20 22:13:54 +0900 with Markdown engine kramdown (1.4.2)
                  using options {}
  -->

<!-- _S9SLIDE_ -->

<ul>
  <li>To improve the reliability of a program</li>
  <li>Development process has to be formalized</li>
  <li>Especially program modifications are important</li>
  <li>Let’s formalize modification using Monad</li>
</ul>


		</section>
</div></div>

<div class="slide" id="3"><div>
		<section>
			<header>
				<h1 id="formalization-using-monad">Formalization using Monad</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>Monad is a notion of Category theory</li>
  <li>Monad represents meta computations in functional program</li>
  <li>We proposed Delta Monad representation of program modifications</li>
  <li>We give definitions and the proof</li>
  <li>Delta Monad can be used with other monads</li>
</ul>


		</section>
</div></div>

<div class="slide" id="4"><div>
		<section>
			<header>
				<h1 id="merits-of-formalizing-program-modifications">Merits of formalizing program modifications</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>Formal methods give verification of program based on mathematics and logics</li>
  <li>Such as lambda calculus and corresponding proofs</li>
  <li>Moggi[1989] , introduce Monad as notion of meta computation in program</li>
  <li>A meta computation represented as a Monad has one to one mapping</li>
  <li>We define program modification as meta computation which includes all modifications</li>
</ul>


		</section>
</div></div>

<div class="slide" id="5"><div>
		<section>
			<header>
				<h1 id="definitions-of-program">Definitions of Program</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>A program is a typed lambda calculus</li>
  <li>lambda term
    <ul>
      <li>variables : x,y</li>
      <li>lambda : \x -&gt; f x</li>
      <li>function applications : f x</li>
    </ul>
  </li>
  <li>type
    <ul>
      <li>type variable   : A, B</li>
      <li>functional type : A -&gt; B</li>
    </ul>
  </li>
</ul>


		</section>
</div></div>

<div class="slide" id="6"><div>
		<section>
			<header>
				<h1 id="every-lambda-term-has-a-type">Every lambda term has a type</h1>
			</header>
			<!-- _S9SLIDE_ -->

<pre><code>    y   :: B
    f   :: A -&gt; B
    f x = y
</code></pre>
<ul>
  <li><code>=</code> is a function definition</li>
  <li><code>f x</code> is a application function <code>f</code></li>
  <li><code>f x</code> has type B</li>
</ul>


		</section>
</div></div>

<div class="slide" id="7"><div>
		<section>
			<header>
				<h1 id="definition-of-delta-in-haskell">Definition of Delta in Haskell</h1>
			</header>
			<!-- _S9SLIDE_ -->

<pre><code>data Delta a = Mono a | Delta a (Delta a)
</code></pre>

<ul>
  <li><code>data</code> is a data type definition in Haskell</li>
  <li><code>a</code> is a type variable</li>
  <li><code>Mono a</code> and <code>Delta a (Delta a)</code> has a type <code>Delta a</code></li>
  <li>Delta can be stores all modification like list structure</li>
</ul>


		</section>
</div></div>

<div class="slide" id="8"><div>
		<section>
			<header>
				<h1 id="how-to-define-meta-computation-in-haskell">How to define meta computation in Haskell</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>original function : f  :: a -&gt; b</li>
  <li>meta function     : f’ :: a -&gt; Monad b</li>
  <li>Original function combination : f ( g ( x ))</li>
  <li>Meta function combination : (x »= f’) »= g’</li>
  <li>f’ returns various value which type is Monad</li>
  <li>Meta computation defined by f’ and <code>&gt;&gt;=</code></li>
  <li>cf. <code>&gt;&gt;=</code> is an infix function</li>
</ul>


		</section>
</div></div>

<div class="slide" id="9"><div>
		<section>
			<header>
				<h1 id="definition-of-delta-meta-computation">Definition of Delta meta computation</h1>
			</header>
			<!-- _S9SLIDE_ -->

<pre><code> &gt;&gt;= :: (Delta a) -&gt; (a -&gt; Delta b) -&gt; (Delta b)
 (Mono x)    &gt;&gt;= f = f x
 (Delta x d) &gt;&gt;= f = Delta (headDelta (f x))
                           (d &gt;&gt;= (tailDelta . f))
</code></pre>

<ul>
  <li>Meta function f is applied to all the versions in a Delta Monad</li>
  <li>Delta data types is accessed by a pattern match</li>
  <li><code>headDelta</code> takes first version of Delta</li>
  <li><code>tailDelta</code> takes the rest versions</li>
</ul>


		</section>
</div></div>

<div class="slide" id="10"><div>
		<section>
			<header>
				<h1 id="an-example-of-program-using-delta-monad">An example of Program using Delta Monad</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>Two versions of a simple program are shown</li>
  <li>Gives Delta Monad representation of the versions</li>
  <li>Various computation can be possible in the Delta</li>
</ul>


		</section>
</div></div>

<div class="slide" id="11"><div>
		<section>
			<header>
				<h1 id="an-example-program-numbercount-version-1">An Example Program: numberCount (Version 1)</h1>
			</header>
			<!-- _S9SLIDE_ -->


<pre><code>generator x     = [1..x]
numberFilter xs = filter isPrime xs
count xs        = length xs

numberCount x = count (numberFilter (generator x))
</code></pre>


		</section>
</div></div>

<div class="slide" id="12"><div>
		<section>
			<header>
				<h1 id="an-example-program-numbercount-version-2">An Example Program: numberCount (Version 2)</h1>
			</header>
			<!-- _S9SLIDE_ -->


<pre><code>generator x     = [1..x]
numberFilter xs = filter even xs
count xs        = length xs

numberCount x = count (numberFilter (generator x))
</code></pre>


		</section>
</div></div>

<div class="slide" id="13"><div>
		<section>
			<header>
				<h1 id="an-example-of-program-includes-two-versions">An Example of Program includes two versions</h1>
			</header>
			<!-- _S9SLIDE_ -->

<pre><code>generator x     = Mono [1..x]
numberFilter xs = Delta (filter even xs)
                        (Mono (filter isPrime xs))
count x         = Mono (length x)

numberCount x = count =&lt;&lt; numberFilter =&lt;&lt; generator x
</code></pre>


		</section>
</div></div>

<div class="slide" id="14"><div>
		<section>
			<header>
				<h1 id="execute-program-includes-two-version">Execute Program includes two version</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>result
    <ul>
      <li>Version 1 : 168</li>
      <li>Version 2 : 500</li>
    </ul>
  </li>
</ul>

<pre><code>*Main&gt; numberCount 1000
Delta 500 (Mono 168)
</code></pre>


		</section>
</div></div>

<div class="slide" id="15"><div>
		<section>
			<header>
				<h1 id="combine-delta-monad-with-other-monads">Combine Delta Monad with other Monads</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>Delta Monad can be used with other monads</li>
  <li>Meta computations can be added function to Delta
    <ul>
      <li>Exception, Logging , I/O, etc…</li>
    </ul>
  </li>
</ul>


		</section>
</div></div>

<div class="slide" id="16"><div>
		<section>
			<header>
				<h1 id="an-example-delta-monad-with-traces">An Example Delta Monad with Traces</h1>
			</header>
			<!-- _S9SLIDE_ -->

<pre><code>*Main&gt; 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"]))))
</code></pre>


		</section>
</div></div>

<div class="slide" id="17"><div>
		<section>
			<header>
				<h1 id="how-to-use-delta-monad-in-program-development">How to use Delta Monad in program development</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>Executing selected versions</li>
  <li>Comparing traces of versions</li>
  <li>Version Control Systems are formalized by Delta Monad</li>
  <li>Combination of other Monads make development more reliable</li>
</ul>


		</section>
</div></div>

<div class="slide" id="18"><div>
		<section>
			<header>
				<h1 id="conclusion">Conclusion</h1>
			</header>
			<!-- _S9SLIDE_ -->

<ul>
  <li>Program Modifications are formal defined</li>
  <li>Program Modifications are meta computation</li>
  <li>Program Modifications are Delta Monad</li>
  <li>Monad-laws are proved in Agda</li>
  <li>Delta Monad include all necessary aspects of modifications?</li>
  <li>What is products/colimits over program versions?</li>
</ul>

<!-- vim: set filetype=markdown.slide: -->
<!-- === end markdown block === -->

		</section>
</div></div>


	<script src="scripts/script.js"></script>
	<!-- Copyright © 2010–2011 Vadim Makeev, http://pepelsbey.net/ -->
</body>
</html>
author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Fri, 20 Feb 2015 22:14:01 +0900
parents	dc01e38c4fc1
children